set B = {0,1};
take
{0,1}
; 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};
{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;
verum
end;
hence
for z being Element of {0,1} holds {0,1} \ {z} is non empty set
; verum