let X be non empty set ; :: thesis: for B being filter_base of X holds <.B.] is Filter of X
let B be filter_base of X; :: thesis: <.B.] is Filter of X
consider b0 being object such that
A1: b0 in B by XBOOLE_0:def 1;
now :: thesis: ( not <.B.] is empty & ( {} in <.B.] implies not {} in <.B.] ) & ( for Y1, Y2 being Subset of X holds
( ( Y1 in <.B.] & Y2 in <.B.] implies Y1 /\ Y2 in <.B.] ) & ( Y1 in <.B.] & Y1 c= Y2 implies Y2 in <.B.] ) ) ) )
thus not <.B.] is empty by A1, def3; :: thesis: ( ( {} in <.B.] implies not {} in <.B.] ) & ( for Y1, Y2 being Subset of X holds
( ( Y1 in <.B.] & Y2 in <.B.] implies Y1 /\ Y2 in <.B.] ) & ( Y1 in <.B.] & Y1 c= Y2 implies Y2 in <.B.] ) ) ) )
hereby :: thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in <.B.] & Y2 in <.B.] implies Y1 /\ Y2 in <.B.] ) & ( Y1 in <.B.] & Y1 c= Y2 implies Y2 in <.B.] ) )
assume A2: {} in <.B.] ; :: thesis: not {} in <.B.]
then reconsider x0 = {} as Subset of X ;
consider b0 being Element of B such that
A3: b0 c= x0 by A2, def3;
thus not {} in <.B.] by A3; :: thesis: verum
end;
let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in <.B.] & Y2 in <.B.] implies Y1 /\ Y2 in <.B.] ) & ( Y1 in <.B.] & Y1 c= Y2 implies Y2 in <.B.] ) )
hereby :: thesis: ( Y1 in <.B.] & Y1 c= Y2 implies Y2 in <.B.] )
assume that
A4: Y1 in <.B.] and
A5: Y2 in <.B.] ; :: thesis: Y1 /\ Y2 in <.B.]
reconsider y1 = Y1, y2 = Y2 as Subset of X ;
consider b1 being Element of B such that
A6: b1 c= y1 by A4, def3;
consider b2 being Element of B such that
A7: b2 c= y2 by A5, def3;
consider b3 being Element of B such that
A8: b3 c= b1 /\ b2 by def4;
b1 /\ b2 c= Y1 /\ Y2 by A6, A7, XBOOLE_1:27;
then b3 c= Y1 /\ Y2 by A8;
hence Y1 /\ Y2 in <.B.] by def3; :: thesis: verum
end;
assume that
A9: Y1 in <.B.] and
A10: Y1 c= Y2 ; :: thesis: Y2 in <.B.]
reconsider y1 = Y1 as Subset of X ;
consider b1 being Element of B such that
A11: b1 c= y1 by A9, def3;
b1 c= Y2 by A10, A11;
hence Y2 in <.B.] by def3; :: thesis: verum
end;
hence <.B.] is Filter of X by CARD_FIL:def 1; :: thesis: verum