theorem lleq_trans: ∀d,T. Transitive … (lleq d T).
/2 width=3 by lleq_llpx_sn_trans/ qed-.
-theorem lleq_canc_sn: â\88\80L,L1,L2,T,d. L â\8b\95[d, T] L1â\86\92 L â\8b\95[d, T] L2 â\86\92 L1 â\8b\95[d, T] L2.
+theorem lleq_canc_sn: â\88\80L,L1,L2,T,d. L â\89¡[d, T] L1â\86\92 L â\89¡[d, T] L2 â\86\92 L1 â\89¡[d, T] L2.
/3 width=3 by lleq_trans, lleq_sym/ qed-.
-theorem lleq_canc_dx: â\88\80L1,L2,L,T,d. L1 â\8b\95[d, T] L â\86\92 L2 â\8b\95[d, T] L â\86\92 L1 â\8b\95[d, T] L2.
+theorem lleq_canc_dx: â\88\80L1,L2,L,T,d. L1 â\89¡[d, T] L â\86\92 L2 â\89¡[d, T] L â\86\92 L1 â\89¡[d, T] L2.
/3 width=3 by lleq_trans, lleq_sym/ qed-.
-(* Note: lleq_nlleq_trans: â\88\80d,T,L1,L. L1â\8b\95[T, d] L →
- â\88\80L2. (L â\8b\95[T, d] L2 â\86\92 â\8a¥) â\86\92 (L1 â\8b\95[T, d] L2 → ⊥).
+(* Note: lleq_nlleq_trans: â\88\80d,T,L1,L. L1â\89¡[T, d] L →
+ â\88\80L2. (L â\89¡[T, d] L2 â\86\92 â\8a¥) â\86\92 (L1 â\89¡[T, d] L2 → ⊥).
/3 width=3 by lleq_canc_sn/ qed-.
works with /4 width=8/ so lleq_canc_sn is more convenient
*)