set B = {0 ,1};
A1:
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
A2:
1
in {0 ,1}
by TARSKI:def 2;
not 1
in {0 }
by TARSKI:def 1;
then A3:
{0 ,1} \ {0 } is non
empty set
by A2, XBOOLE_0:def 5;
A4:
0 in {0 ,1}
by TARSKI:def 2;
not
0 in {1}
by TARSKI:def 1;
then
{0 ,1} \ {1} is non
empty set
by A4, XBOOLE_0:def 5;
hence
{0 ,1} \ {z} is non
empty set
by A3, TARSKI:def 2;
:: thesis: verum
end;
take
{0 ,1}
; :: thesis: for z being Element of {0 ,1} holds {0 ,1} \ {z} is non empty set
thus
for z being Element of {0 ,1} holds {0 ,1} \ {z} is non empty set
by A1; :: thesis: verum