let B, C be set ; :: thesis: ( ( 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) ) ) ; :: thesis: B = C
thus B c= C :: according to XBOOLE_0:def 10 :: thesis: C c= B
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in B or p in C )
assume p in B ; :: thesis: p in C
then ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) by A5;
hence p in C by A6; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in C or p in B )
assume p in C ; :: thesis: 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; :: thesis: verum