let
X
be non
empty
set
;
:: thesis:
for
F
being
Filter
of
X
holds
X
in
F
let
F
be
Filter
of
X
;
:: thesis:
X
in
F
set
Y
= the
Element
of
F
;
( the
Element
of
F
in
F
&
X
c=
X
) ;
hence
X
in
F
by
Def1
;
:: thesis:
verum