∀G2,L2,U2. ⦃F2,K2,T2⦄ ≻[h] ⦃G2,L2,U2⦄ →
∃∃G1,L1,U1. ⦃F1,K1,T1⦄ ≻[h] ⦃G1,L1,U1⦄ & ⦃G1,L1,U1⦄ ≥[h] ⦃G2,L2,U2⦄.
#h #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H
∀G2,L2,U2. ⦃F2,K2,T2⦄ ≻[h] ⦃G2,L2,U2⦄ →
∃∃G1,L1,U1. ⦃F1,K1,T1⦄ ≻[h] ⦃G1,L1,U1⦄ & ⦃G1,L1,U1⦄ ≥[h] ⦃G2,L2,U2⦄.
#h #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H