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