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

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

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

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

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

hence x in X /\ (X \/ Y) by A1, XBOOLE_0:def 4; :: thesis: verum

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

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

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

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

hence x in X /\ (X \/ Y) by A1, XBOOLE_0:def 4; :: thesis: verum