let X be non empty set ; :: thesis: 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; :: thesis: { 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

proof

A2: A in { B where B is Subset of X : A c= B } ;

now :: thesis: for x being object st x in { B where B is Subset of X : A c= B } holds
x in bool X

let x be object ; :: thesis: ( x in { B where B is Subset of X : A c= B } implies x in bool X )
assume A3: x in { B where B is Subset of X : A c= B } ; :: thesis: x in bool X
consider b0 being Subset of X such that
A4: x = b0 and
A c= b0 by A3;
thus x in bool X by A4; :: thesis: verum

end;

then { B where B is Subset of X : A c= B } c= bool X ;
hence { B where B is Subset of X : A c= B } is non empty Subset-Family of X by A2; :: thesis: verum

end;

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 } ; :: thesis: contradiction
then consider b0 being Subset of X such that
A6: ( {} = b0 & A c= b0 ) ;
thus contradiction by A6; :: thesis: 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 }

proof

let Y1, Y2 be Subset of X; :: thesis: ( Y1 in { B where B is Subset of X : A c= B } & Y2 in { B where B is Subset of X : A c= B } implies Y1 /\ Y2 in { B where B is Subset of X : A c= B } )
assume that
A8: Y1 in { B where B is Subset of X : A c= B } and
A9: Y2 in { B where B is Subset of X : A c= B } ; :: thesis: Y1 /\ Y2 in { B where B is Subset of X : A c= B }
consider b1 being Subset of X such that
A10: ( Y1 = b1 & A c= b1 ) by A8;
consider b2 being Subset of X such that
A11: ( Y2 = b2 & A c= b2 ) by A9;
A c= Y1 /\ Y2 by A10, A11, XBOOLE_1:19;
hence Y1 /\ Y2 in { B where B is Subset of X : A c= B } ; :: thesis: verum

end;

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; :: thesis: ( 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 ; :: thesis: 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 } ; :: thesis: 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; :: thesis: verum