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

assume A1: X c= Y ; :: thesis: X \/ Y = Y

thus X \/ Y c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= X \/ Y

thus ( not x in Y or x in X \/ Y ) by XBOOLE_0:def 3; :: thesis: verum

assume A1: X c= Y ; :: thesis: X \/ Y = Y

thus X \/ Y c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= X \/ Y

proof

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

assume x in X \/ Y ; :: thesis: x in Y

then ( x in X or x in Y ) by XBOOLE_0:def 3;

hence x in Y by A1; :: thesis: verum

end;assume x in X \/ Y ; :: thesis: x in Y

then ( x in X or x in Y ) by XBOOLE_0:def 3;

hence x in Y by A1; :: thesis: verum

thus ( not x in Y or x in X \/ Y ) by XBOOLE_0:def 3; :: thesis: verum