let
X
be non
empty
set
;
:: thesis:
for
I
being
Ideal
of
X
holds
{}
in
I
let
I
be
Ideal
of
X
;
:: thesis:
{}
in
I
set
Y
= the
Element
of
I
;
(
{}
c=
the
Element
of
I
&
{}
c=
X
) ;
hence
{}
in
I
by
Def2
;
:: thesis:
verum