(* Basic_2A1: uses: csx_lleq_conf *)
lemma csx_reqg_conf (S) (G) (T):
reflexive … S → symmetric … S →
- â\88\80L1. â\9dªG,L1â\9d« ⊢ ⬈*𝐒 T →
- â\88\80L2. L1 â\89\9b[S,T] L2 â\86\92 â\9dªG,L2â\9d« ⊢ ⬈*𝐒 T.
+ â\88\80L1. â\9d¨G,L1â\9d© ⊢ ⬈*𝐒 T →
+ â\88\80L2. L1 â\89\9b[S,T] L2 â\86\92 â\9d¨G,L2â\9d© ⊢ ⬈*𝐒 T.
#S #G #T #H1S #H2S #L1 #H
@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
@csx_intro #T2 #HT12 #HnT12
(* Basic_2A1: uses: csx_lleq_trans *)
lemma csx_reqg_trans (S) (G) (T):
reflexive … S → symmetric … S →
- â\88\80L1,L2. L1 â\89\9b[S,T] L2 â\86\92 â\9dªG,L2â\9d« â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\9dªG,L1â\9d« ⊢ ⬈*𝐒 T.
+ â\88\80L1,L2. L1 â\89\9b[S,T] L2 â\86\92 â\9d¨G,L2â\9d© â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\9d¨G,L1â\9d© ⊢ ⬈*𝐒 T.
/3 width=8 by csx_reqg_conf, reqg_sym/ qed-.