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

assume x in {1} ; :: thesis: x in 2 \ 1

then A3: x = 1 by TARSKI:def 1;

then A4: not x in {0} by TARSKI:def 1;

x in {0,1} by A3, TARSKI:def 2;

hence x in 2 \ 1 by A4, CARD_1:49, CARD_1:50, XBOOLE_0:def 5; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in 2 \ 1 )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 2 \ 1 or x in {1} )

assume A1: x in 2 \ 1 ; :: thesis: x in {1}

then A2: ( x = 0 or x = 1 ) by CARD_1:50, TARSKI:def 2;

not x in {0} by A1, CARD_1:49, XBOOLE_0:def 5;

hence x in {1} by A2, TARSKI:def 1; :: thesis: verum

end;assume A1: x in 2 \ 1 ; :: thesis: x in {1}

then A2: ( x = 0 or x = 1 ) by CARD_1:50, TARSKI:def 2;

not x in {0} by A1, CARD_1:49, XBOOLE_0:def 5;

hence x in {1} by A2, TARSKI:def 1; :: thesis: verum

assume x in {1} ; :: thesis: x in 2 \ 1

then A3: x = 1 by TARSKI:def 1;

then A4: not x in {0} by TARSKI:def 1;

x in {0,1} by A3, TARSKI:def 2;

hence x in 2 \ 1 by A4, CARD_1:49, CARD_1:50, XBOOLE_0:def 5; :: thesis: verum