/3 width=9 by fpbs_strap1, fpbq_feqx/ qed-.
(* Basic_2A1: uses: lleq_fpbs_trans *)
lemma feqx_fpbs_trans:
∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ →
/3 width=9 by fpbs_strap1, fpbq_feqx/ qed-.
(* Basic_2A1: uses: lleq_fpbs_trans *)
lemma feqx_fpbs_trans:
∀G,G2,L,L2,T,T2. ❪G,L,T❫ ≥ ❪G2,L2,T2❫ →