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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 3 \ 2 or x in {2} )
assume A1: x in 3 \ 2 ; :: thesis: x in {2}
then A2: ( x = 0 or x = 1 or x = 2 ) by CARD_1:51, ENUMSET1:def 1;
not x in {0,1} by A1, CARD_1:50, XBOOLE_0:def 5;
hence x in {2} by A2, TARSKI:def 1, TARSKI:def 2; :: thesis: verum

end;

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

proof

let x be object ; :: 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 A3: x = 2 by TARSKI:def 1;
then A4: not x in {0,1} by TARSKI:def 2;
x in {0,1,2} by A3, ENUMSET1:def 1;
hence x in 3 \ 2 by A4, CARD_1:50, CARD_1:51, XBOOLE_0:def 5; :: thesis: verum

end;