let X, x1, x2 be set ; :: thesis: for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R#3e S)} c= D & X is D -expanded & [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) & (r -compound) . x1 in X holds
(r -compound) . x2 in X
let S be Language; :: thesis: for r being relational Element of S
for D being RuleSet of S st {(R#3e S)} c= D & X is D -expanded & [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) & (r -compound) . x1 in X holds
(r -compound) . x2 in X
let r be relational Element of S; :: thesis: for D being RuleSet of S st {(R#3e S)} c= D & X is D -expanded & [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) & (r -compound) . x1 in X holds
(r -compound) . x2 in X
let D be RuleSet of S; :: thesis: ( {(R#3e S)} c= D & X is D -expanded & [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) & (r -compound) . x1 in X implies (r -compound) . x2 in X )
set s = r;
set n = |.(ar r).|;
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set f = r -compound ;
set R = (X,D) -termEq ;
assume A1: {(R#3e S)} c= D ; :: thesis: ( not X is D -expanded or not [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) or not (r -compound) . x1 in X or (r -compound) . x2 in X )
assume A2: X is D -expanded ; :: thesis: ( not [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) or not (r -compound) . x1 in X or (r -compound) . x2 in X )
assume [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) ; :: thesis: ( not (r -compound) . x1 in X or (r -compound) . x2 in X )
then consider T1, T2 being |.(ar r).| -element Element of (AllTermsOf S) * such that
A3: ( T1 = x1 & T2 = x2 & PairWiseEq (T1,T2) c= X ) by Lm37, A2;
set Z = PairWiseEq (T1,T2);
reconsider w1 = r -compound T1, w2 = r -compound T2 as 0 -wff string of S ;
A4: ( (r -compound) . x1 = w1 & (r -compound) . x2 = w2 ) by A3, FOMODEL3:def 2;
assume (r -compound) . x1 in X ; :: thesis: (r -compound) . x2 in X
then reconsider X1 = {w1} as Subset of X by ZFMISC_1:31, A4;
reconsider ZZ = PairWiseEq (T1,T2) as Subset of X by A3;
reconsider ZZZ = ZZ \/ X1 as Subset of X ;
{[((PairWiseEq (T1,T2)) \/ {(r -compound T1)}),(r -compound T2)]} is {} ,{(R#3e S)} -derivable ;
then {[ZZZ,w2]} is {} ,D -derivable by Lm18, A1;
then w2 is ZZZ,D -provable ;
then {w2} c= X by A2;
hence (r -compound) . x2 in X by A4, ZFMISC_1:31; :: thesis: verum