thus 3 \ 2 c= {2} :: according to XBOOLE_0:def 10 :: thesis: {2} c= 3 \ 2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in 3 \ 2 or x in {2} )
assume x in 3 \ 2 ; :: thesis: x in {2}
then ( x in {0 ,1,2} & not x in {0 ,1} ) by CARD_1:88, CARD_1:89, XBOOLE_0:def 5;
then ( ( x = 0 or x = 1 or x = 2 ) & x <> 0 & x <> 1 ) by ENUMSET1:def 1, TARSKI:def 2;
hence x in {2} by TARSKI:def 1; :: thesis: verum

end;

thus {2} c= 3 \ 2 :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {2} or x in 3 \ 2 )
assume x in {2} ; :: thesis: x in 3 \ 2
then x = 2 by TARSKI:def 1;
then ( x in {0 ,1,2} & not x in {0 ,1} ) by ENUMSET1:def 1, TARSKI:def 2;
hence x in 3 \ 2 by CARD_1:88, CARD_1:89, XBOOLE_0:def 5; :: thesis: verum

end;