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

proof

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

end;

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

proof

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

end;