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 (abs (ar s)) -placesOf ((X,D) -termEq) holds
ex T, U being abs (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 (abs (ar s)) -placesOf ((X,D) -termEq) holds
ex T, U being abs (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 (abs (ar s)) -placesOf ((X,D) -termEq) holds
ex T, U being abs (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 (abs (ar s)) -placesOf ((X,D) -termEq) implies ex T, U being abs (ar s) -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X ) )
set n = abs (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 B4: X is D -expanded ; :: thesis: ( not [x1,x2] in (abs (ar s)) -placesOf ((X,D) -termEq) or ex T, U being abs (ar s) -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X ) )
assume [x1,x2] in (abs (ar s)) -placesOf ((X,D) -termEq) ; :: thesis: ex T, U being abs (ar s) -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X )
then consider p, q being Element of (abs (ar s)) -tuples_on (AllTermsOf S) such that
B2: ( [x1,x2] = [p,q] & ( for i being set st i in Seg (abs (ar s)) holds
[(p . i),(q . i)] in (X,D) -termEq ) ) ;
B3: ( p = x1 & q = x2 ) by B2, ZFMISC_1:27;
reconsider T1 = x1, T2 = x2 as Element of (abs (ar s)) -tuples_on (AllTermsOf S) by B2, ZFMISC_1:27;
reconsider T11 = T1, T22 = T2 as abs (ar s) -element Element of (AllTermsOf S) * by FINSEQ_1:def 11;
take T = T11; :: thesis: ex U being abs (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 (abs (ar s))),(AllTermsOf S)) & T2 is Element of Funcs ((Seg (abs (ar s))),(AllTermsOf S)) ) by FOMODEL0:11;
then reconsider T111 = T1, T222 = T2 as Function of (Seg (abs (ar s))),(AllTermsOf S) ;

now

let z be set ; :: 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 (abs (ar s)), TT, UU being Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) such that
C0: ( 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 B2, B3;
then (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable by Lm23;
then {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} c= X by B4, DefExpanded;
hence z in X by C0, ZFMISC_1:31; :: thesis: verum

end;

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