let S be Language; :: thesis: for s being relational Element of S
for T1, T2 being |.(ar b₁).| -element Element of (AllTermsOf S) * holds {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R#3e S)} -derivable
let s be relational Element of S; :: thesis: for T1, T2 being |.(ar s).| -element Element of (AllTermsOf S) * holds {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R#3e S)} -derivable
set m = |.(ar s).|;
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set AF = AllFormulasOf S;
let T1, T2 be |.(ar s).| -element Element of (AllTermsOf S) * ; :: thesis: {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R#3e 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 Def2;
reconsider Seqts = {} as Subset of (S -sequents) by XBOOLE_1:2;
seqt Rule3e Seqts ;
then [Seqts,seqt] in P#3e S by Def40;
then seqt in (R#3e S) . Seqts by Lm27;
hence {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R#3e S)} -derivable by Lm20, ZFMISC_1:31; :: thesis: verum