let S be Language; :: thesis: for s being relational Element of S
for T1, T2 being abs (ar b₁) -element Element of (AllTermsOf S) * holds {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R3e S)} -derivable
let s be relational Element of S; :: thesis: for T1, T2 being abs (ar s) -element Element of (AllTermsOf S) * holds {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R3e S)} -derivable
set m = abs (ar s);
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set AF = AllFormulasOf S;
let T1, T2 be abs (ar s) -element Element of (AllTermsOf S) * ; :: thesis: {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R3e S)} -derivable
reconsider w1 = s -compound T1, conclusion = s -compound T2 as 0 -wff string of S ;
w1 in AllFormulasOf S ;
then reconsider w11 = w1 as Element of AllFormulasOf S ;
reconsider premises = (PairWiseEq (T1,T2)) \/ {w11} as Subset of (AllFormulasOf S) ;
reconsider seqt = [premises,conclusion] as Element of S -sequents by DefSeqtLike;
reconsider Seqts = {} as Subset of (S -sequents) by XBOOLE_1:2;
( seqt `1 = {(s -compound T1)} \/ (PairWiseEq (T1,T2)) & seqt `2 = s -compound T2 ) by MCART_1:7;
then seqt Rule3e Seqts by Def3e;
then [Seqts,seqt] in P3e S by DefP3e;
then seqt in (R3e S) . Seqts by Lm1;
then {seqt} c= (R3e S) . Seqts by ZFMISC_1:31;
hence {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R3e S)} -derivable by Lm9; :: thesis: verum