let X, Y be set ; :: thesis: X /\ Y c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ Y or x in X )
thus ( not x in X /\ Y or x in X ) by XBOOLE_0:def 4; :: thesis: verum