thus ( X = Y implies for c being Complex holds
( c in X iff c in Y ) ) ; :: thesis: ( ( for c being Complex holds
( c in X iff c in Y ) ) implies X = Y )
assume for c being Complex holds
( c in X iff c in Y ) ; :: thesis: X = Y
hence ( X c= Y & Y c= X ) ; :: according to XBOOLE_0:def 10 :: thesis: verum