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 {(R3e S)} c= D & X is D -expanded & [x1,x2] in (abs (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 {(R3e S)} c= D & X is D -expanded & [x1,x2] in (abs (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 {(R3e S)} c= D & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) & (r -compound) . x1 in X holds
(r -compound) . x2 in X
let D be RuleSet of S; :: thesis: ( {(R3e S)} c= D & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) & (r -compound) . x1 in X implies (r -compound) . x2 in X )
set s = r;
set n = abs (ar r);
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set f = r -compound ;
set R = (X,D) -termEq ;
assume B1: {(R3e S)} c= D ; :: thesis: ( not X is D -expanded or not [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) or not (r -compound) . x1 in X or (r -compound) . x2 in X )
assume B2: X is D -expanded ; :: thesis: ( not [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) or not (r -compound) . x1 in X or (r -compound) . x2 in X )
assume [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) ; :: thesis: ( not (r -compound) . x1 in X or (r -compound) . x2 in X )
then consider T1, T2 being abs (ar r) -element Element of (AllTermsOf S) * such that
B0: ( T1 = x1 & T2 = x2 & PairWiseEq (T1,T2) c= X ) by Lm42, B2;
set Z = PairWiseEq (T1,T2);
reconsider w1 = r -compound T1, w2 = r -compound T2 as 0 -wff string of S ;
B4: ( (r -compound) . x1 = w1 & (r -compound) . x2 = w2 ) by B0, FOMODEL3:def 2;
assume (r -compound) . x1 in X ; :: thesis: (r -compound) . x2 in X
then reconsider X1 = {w1} as Subset of X by B4, ZFMISC_1:31;
reconsider ZZ = PairWiseEq (T1,T2) as Subset of X by B0;
reconsider ZZZ = ZZ \/ X1 as Subset of X ;
{[((PairWiseEq (T1,T2)) \/ {(r -compound T1)}),(r -compound T2)]} is {} ,{(R3e S)} -derivable ;
then {[ZZZ,w2]} is {} ,D -derivable by Lm20, B1;
then w2 is ZZZ,D -provable by DefProvable;
then {w2} c= X by B2, DefExpanded;
hence (r -compound) . x2 in X by B4, ZFMISC_1:31; :: thesis: verum