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

proof

thus
{1,2} c= 3 \ 1
:: thesis: verum
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;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

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;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