(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
lemma req_inv_lifts_bi: âL1,L2,U. L1 âĄ[U] L2 â âb,f. đâŚf⌠â
- âK1,K2. âŹ*[b, f] L1 â K1 â âŹ*[b, f] L2 â K2 â
+ âK1,K2. âŹ*[b,f] L1 â K1 â âŹ*[b,f] L2 â K2 â
âT. âŹ*[f] T â U â K1 âĄ[T] K2.
/2 width=10 by rex_inv_lifts_bi/ qed-.