let B, C be set ; ( ( for p being set holds
( p in B iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) & ( for p being set holds
( p in C iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) ) implies B = C )
assume that
A5:
for p being set holds
( p in B iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )
and
A6:
for p being set holds
( p in C iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) )
; B = C
thus
B c= C
XBOOLE_0:def 10 C c= B
let p be object ; TARSKI:def 3 ( not p in C or p in B )
assume
p in C
; p in B
then
ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) )
by A6;
hence
p in B
by A5; verum