let X, Y, Z be set ; :: thesis: ( X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z )

assume that

A1: X \/ Y = Z \/ Y and

A2: X /\ Y = {} and

A3: Z /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: X = Z

thus X c= Z :: according to XBOOLE_0:def 10 :: thesis: Z c= X

assume A6: x in Z ; :: thesis: x in X

Z c= X \/ Y by A1, Th7;

then A7: x in X \/ Y by A6;

not x in Y by A3, A6, XBOOLE_0:def 4;

hence x in X by A7, XBOOLE_0:def 3; :: thesis: verum

assume that

A1: X \/ Y = Z \/ Y and

A2: X /\ Y = {} and

A3: Z /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: X = Z

thus X c= Z :: according to XBOOLE_0:def 10 :: thesis: Z c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in X )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )

assume A4: x in X ; :: thesis: x in Z

X c= Z \/ Y by A1, Th7;

then A5: x in Z \/ Y by A4;

not x in Y by A2, A4, XBOOLE_0:def 4;

hence x in Z by A5, XBOOLE_0:def 3; :: thesis: verum

end;assume A4: x in X ; :: thesis: x in Z

X c= Z \/ Y by A1, Th7;

then A5: x in Z \/ Y by A4;

not x in Y by A2, A4, XBOOLE_0:def 4;

hence x in Z by A5, XBOOLE_0:def 3; :: thesis: verum

assume A6: x in Z ; :: thesis: x in X

Z c= X \/ Y by A1, Th7;

then A7: x in X \/ Y by A6;

not x in Y by A3, A6, XBOOLE_0:def 4;

hence x in X by A7, XBOOLE_0:def 3; :: thesis: verum