set B = {0,1};
take {0,1} ; :: thesis: for z being Element of {0,1} holds {0,1} \ {z} is non empty set
for z being Element of {0,1} holds {0,1} \ {z} is non empty set
proof
let z be Element of {0,1}; :: thesis: {0,1} \ {z} is non empty set
( 0 in {0,1} & not 0 in {1} ) by TARSKI:def 1, TARSKI:def 2;
then A1: {0,1} \ {1} is non empty set by XBOOLE_0:def 5;
( 1 in {0,1} & not 1 in {0} ) by TARSKI:def 1, TARSKI:def 2;
then {0,1} \ {0} is non empty set by XBOOLE_0:def 5;
hence {0,1} \ {z} is non empty set by A1, TARSKI:def 2; :: thesis: verum
end;
hence for z being Element of {0,1} holds {0,1} \ {z} is non empty set ; :: thesis: verum