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