let X be non empty set ; for A being non empty Subset of X holds { B where B is Subset of X : A c= B } is Filter of X
let A be non empty Subset of X; { B where B is Subset of X : A c= B } is Filter of X
set C = { B where B is Subset of X : A c= B } ;
A1:
{ B where B is Subset of X : A c= B } is non empty Subset-Family of X
A5:
not {} in { B where B is Subset of X : A c= B }
proof
assume
{} in { B where B is Subset of X : A c= B }
;
contradiction
then consider b0 being
Subset of
X such that A6:
(
{} = b0 &
A c= b0 )
;
thus
contradiction
by A6;
verum
end;
A7:
for Y1, Y2 being Subset of X st Y1 in { B where B is Subset of X : A c= B } & Y2 in { B where B is Subset of X : A c= B } holds
Y1 /\ Y2 in { B where B is Subset of X : A c= B }
for Y1, Y2 being Subset of X st Y1 in { B where B is Subset of X : A c= B } & Y1 c= Y2 holds
Y2 in { B where B is Subset of X : A c= B }
proof
let Y1,
Y2 be
Subset of
X;
( Y1 in { B where B is Subset of X : A c= B } & Y1 c= Y2 implies Y2 in { B where B is Subset of X : A c= B } )
assume that A12:
Y1 in { B where B is Subset of X : A c= B }
and A13:
Y1 c= Y2
;
Y2 in { B where B is Subset of X : A c= B }
consider b1 being
Subset of
X such that A14:
(
b1 = Y1 &
A c= b1 )
by A12;
A c= Y2
by A13, A14;
hence
Y2 in { B where B is Subset of X : A c= B }
;
verum
end;
hence
{ B where B is Subset of X : A c= B } is Filter of X
by A1, A5, A7, CARD_FIL:def 1; verum