let x be object ; :: thesis: for X being set holds
( {x} c= X iff x in X )
let X be set ; :: thesis: ( {x} c= X iff x in X )
x in {x} by TARSKI:def 1;
hence ( {x} c= X implies x in X ) ; :: thesis: ( x in X implies {x} c= X )
assume A1: x in X ; :: thesis: {x} c= X
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {x} or y in X )
thus ( not y in {x} or y in X ) by A1, TARSKI:def 1; :: thesis: verum