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

proof

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

end;

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

proof

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

end;