let x, X be set ; :: thesis: ( {x} c= X iff x in X )
thus ( {x} c= X implies x in X ) :: thesis: ( x in X implies {x} c= X )

proof

x in {x} by TARSKI:def 1;
hence ( {x} c= X implies x in X ) by TARSKI:def 3; :: thesis: verum

end;

assume A1: x in X ; :: thesis: {x} c= X
let y be set ; :: 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