let x, y be object ; :: thesis: for Z being set st {x,y} \/ Z c= Z holds
x in Z
let Z be set ; :: thesis: ( {x,y} \/ Z c= Z implies x in Z )
assume A1: {x,y} \/ Z c= Z ; :: thesis: x in Z
assume not x in Z ; :: thesis: contradiction
then not x in {x,y} \/ Z by A1;
then not x in {x,y} by XBOOLE_0:def 3;
hence contradiction by TARSKI:def 2; :: thesis: verum