thus 2 \ 1 c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= 2 \ 1
proof
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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in 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