let X, x1, x2 be set ; :: thesis: for S being Language
for D being RuleSet of S
for s being low-compounding Element of S st X is D -expanded & [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) holds
ex T, U being |.(ar b₃).| -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X )
let S be Language; :: thesis: for D being RuleSet of S
for s being low-compounding Element of S st X is D -expanded & [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) holds
ex T, U being |.(ar b₂).| -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X )
let D be RuleSet of S; :: thesis: for s being low-compounding Element of S st X is D -expanded & [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) holds
ex T, U being |.(ar b₁).| -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X )
let s be low-compounding Element of S; :: thesis: ( X is D -expanded & [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) implies ex T, U being |.(ar s).| -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X ) )
set n = |.(ar s).|;
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set f = S -cons ;
set SS = AllSymbolsOf S;
set R = (X,D) -termEq ;
set SS = AllSymbolsOf S;
assume A1: X is D -expanded ; :: thesis: ( not [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) or ex T, U being |.(ar s).| -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X ) )
assume [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) ; :: thesis: ex T, U being |.(ar s).| -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X )
then consider p, q being Element of |.(ar s).| -tuples_on (AllTermsOf S) such that
A2: ( [x1,x2] = [p,q] & ( for i being set st i in Seg |.(ar s).| holds
[(p . i),(q . i)] in (X,D) -termEq ) ) ;
A3: ( p = x1 & q = x2 ) by A2, XTUPLE_0:1;
reconsider T1 = x1, T2 = x2 as Element of |.(ar s).| -tuples_on (AllTermsOf S) by A2, XTUPLE_0:1;
reconsider T11 = T1, T22 = T2 as |.(ar s).| -element Element of (AllTermsOf S) * by FINSEQ_1:def 11;
take T = T11; :: thesis: ex U being |.(ar s).| -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X )
take U = T22; :: thesis: ( T = x1 & U = x2 & PairWiseEq (T,U) c= X )
thus ( T = x1 & U = x2 ) ; :: thesis: PairWiseEq (T,U) c= X
set Z = PairWiseEq (T,U);
( T1 is Element of Funcs ((Seg |.(ar s).|),(AllTermsOf S)) & T2 is Element of Funcs ((Seg |.(ar s).|),(AllTermsOf S)) ) by FOMODEL0:11;
then reconsider T111 = T1, T222 = T2 as Function of (Seg |.(ar s).|),(AllTermsOf S) ;

now :: thesis: for z being object st z in PairWiseEq (T,U) holds
z in X

let z be object ; :: thesis: ( z in PairWiseEq (T,U) implies z in X )
assume z in PairWiseEq (T,U) ; :: thesis: z in X
then consider j being Element of Seg |.(ar s).|, TT, UU being Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) such that
A4: ( z = (<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j) & TT = T11 & UU = T22 ) ;
reconsider t11 = T111 . j, t22 = T222 . j as Element of AllTermsOf S ;
reconsider t1 = t11, t2 = t22 as termal string of S ;
[(T111 . j),(T222 . j)] in (X,D) -termEq by A2, A3;
then (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable by Lm23;
then {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} c= X by A1;
hence z in X by A4, ZFMISC_1:31; :: thesis: verum

end;

hence PairWiseEq (T,U) c= X by TARSKI:def 3; :: thesis: verum