let E be set ; :: thesis: for A, B being Subset of E st ( for x being Element of E holds
( x in A iff x in B ) ) holds
A = B
let A, B be Subset of E; :: thesis: ( ( for x being Element of E holds
( x in A iff x in B ) ) implies A = B )
assume for x being Element of E holds
( x in A iff x in B ) ; :: thesis: A = B
hence ( A c= B & B c= A ) by Th7; :: according to XBOOLE_0:def 10 :: thesis: verum