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

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

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

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

proof

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

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

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

hence x in X by XBOOLE_0:def 4; :: thesis: verum

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

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

hence x in X by XBOOLE_0:def 4; :: thesis: verum

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