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
A4: 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
A5: 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 set ; :: 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 A4;
hence p in C by A5; :: thesis: verum

end;

let p be set ; :: 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 A5;
hence p in B by A4; :: thesis: verum