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

proof

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

end;

let x be set ; :: 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 x = 1 by TARSKI:def 1;
then ( x in {0 ,1} & not x in {0 } ) by TARSKI:def 1, TARSKI:def 2;
hence x in 2 \ 1 by CARD_1:87, CARD_1:88, XBOOLE_0:def 5; :: thesis: verum