{}
P
in
{
X
where
X
is
Subset
of
P
:
X
is
lower
}
;
hence
{
X
where
X
is
Subset
of
P
:
X
is
lower
} is non
empty
set
;
:: thesis:
verum