let X, Y be set ; :: thesis: ( X c= Y \ X implies X = {} )

assume A1: X c= Y \ X ; :: thesis: X = {}

thus X c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= X

assume A1: X c= Y \ X ; :: thesis: X = {}

thus X c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= X

proof

thus
{} c= X
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {} )

assume A2: x in X ; :: thesis: x in {}

then x in Y \ X by A1;

hence x in {} by A2, XBOOLE_0:def 5; :: thesis: verum

end;assume A2: x in X ; :: thesis: x in {}

then x in Y \ X by A1;

hence x in {} by A2, XBOOLE_0:def 5; :: thesis: verum