theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2.
⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 *
-/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpb_lleq/
+/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_lleq/
qed-.
(* Advanced properties ******************************************************)