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