let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for A being non empty set
for J being interpretation of A st ( for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in A st v | (still_not-bound_in (All x,p)) = w | (still_not-bound_in (All x,p)) holds
( J,v |= All x,p iff J,w |= All x,p )
let x be bound_QC-variable; :: thesis: for A being non empty set
for J being interpretation of A st ( for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in A st v | (still_not-bound_in (All x,p)) = w | (still_not-bound_in (All x,p)) holds
( J,v |= All x,p iff J,w |= All x,p )
let A be non empty set ; :: thesis: for J being interpretation of A st ( for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in A st v | (still_not-bound_in (All x,p)) = w | (still_not-bound_in (All x,p)) holds
( J,v |= All x,p iff J,w |= All x,p )
let J be interpretation of A; :: thesis: ( ( for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) implies for v, w being Element of Valuations_in A st v | (still_not-bound_in (All x,p)) = w | (still_not-bound_in (All x,p)) holds
( J,v |= All x,p iff J,w |= All x,p ) )
assume A1: for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ; :: thesis: for v, w being Element of Valuations_in A st v | (still_not-bound_in (All x,p)) = w | (still_not-bound_in (All x,p)) holds
( J,v |= All x,p iff J,w |= All x,p )
let v, w be Element of Valuations_in A; :: thesis: ( v | (still_not-bound_in (All x,p)) = w | (still_not-bound_in (All x,p)) implies ( J,v |= All x,p iff J,w |= All x,p ) )
assume A2: v | (still_not-bound_in (All x,p)) = w | (still_not-bound_in (All x,p)) ; :: thesis: ( J,v |= All x,p iff J,w |= All x,p )
set X = (still_not-bound_in p) \ {x};
v | (still_not-bound_in (All x,p)) = v | ((still_not-bound_in p) \ {x}) by QC_LANG3:16;
then A3: v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) by A2, QC_LANG3:16;
( ( for a being Element of A holds J,v . (x | a) |= p ) iff for a being Element of A holds J,w . (x | a) |= p )

proof

thus ( ( for a being Element of A holds J,v . (x | a) |= p ) implies for a being Element of A holds J,w . (x | a) |= p ) :: thesis: ( ( for a being Element of A holds J,w . (x | a) |= p ) implies for a being Element of A holds J,v . (x | a) |= p )

proof

assume A4: for a being Element of A holds J,v . (x | a) |= p ; :: thesis: for a being Element of A holds J,w . (x | a) |= p
let a be Element of A; :: thesis: J,w . (x | a) |= p
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p) by A3, Th67;
then ( J,v . (x | a) |= p iff J,w . (x | a) |= p ) by A1;
hence J,w . (x | a) |= p by A4; :: thesis: verum

end;

thus ( ( for a being Element of A holds J,w . (x | a) |= p ) implies for a being Element of A holds J,v . (x | a) |= p ) :: thesis: verum

proof

assume A5: for a being Element of A holds J,w . (x | a) |= p ; :: thesis: for a being Element of A holds J,v . (x | a) |= p
let a be Element of A; :: thesis: J,v . (x | a) |= p
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p) by A3, Th67;
then ( J,v . (x | a) |= p iff J,w . (x | a) |= p ) by A1;
hence J,v . (x | a) |= p by A5; :: thesis: verum

end;

end;

hence ( J,v |= All x,p iff J,w |= All x,p ) by Th51; :: thesis: verum