(* Basic_2A1: fpb_fpbq_alt *)
lemma fpb_fpbq_ffdneq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ →
∧∧ ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ & (⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⊥).
(* Basic_2A1: fpb_fpbq_alt *)
lemma fpb_fpbq_ffdneq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ →
∧∧ ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ & (⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⊥).