let E be set ; :: thesis: for A, B being Subset of E st ( for x being Element of E holds
( not 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
( not x in A iff x in B ) ) implies A = B ` )
assume for x being Element of E holds
( not x in A iff x in B ) ; :: thesis: A = B `
then for x being Element of E holds
( x in A iff not x in B ) ;
hence A = B ` by Th30; :: thesis: verum