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