let X be non empty set ; :: thesis: for Z being Subset of X
for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter F,Z & Extend_Filter F,Z is Filter of X & F c= Extend_Filter F,Z )
let Z be Subset of X; :: thesis: for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter F,Z & Extend_Filter F,Z is Filter of X & F c= Extend_Filter F,Z )
let F be Filter of X; :: thesis: ( ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) implies ( Z in Extend_Filter F,Z & Extend_Filter F,Z is Filter of X & F c= Extend_Filter F,Z ) )
assume A1: for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ; :: thesis: ( Z in Extend_Filter F,Z & Extend_Filter F,Z is Filter of X & F c= Extend_Filter F,Z )
( X in F & X /\ Z c= Z ) by Th5, XBOOLE_1:17;
hence Z in Extend_Filter F,Z by Th13; :: thesis: ( Extend_Filter F,Z is Filter of X & F c= Extend_Filter F,Z )
thus Extend_Filter F,Z is Filter of X :: thesis: F c= Extend_Filter F,Z

proof

thus not {} in Extend_Filter F,Z :: according to CARD_FIL:def 1 :: thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in Extend_Filter F,Z & Y2 in Extend_Filter F,Z implies Y1 /\ Y2 in Extend_Filter F,Z ) & ( Y1 in Extend_Filter F,Z & Y1 c= Y2 implies Y2 in Extend_Filter F,Z ) )

proof

assume {} in Extend_Filter F,Z ; :: thesis: contradiction
then consider Z2 being Subset of X such that
A2: Z2 in F and
A3: Z2 /\ Z c= {} by Th13;
Z2 meets Z by A1, A2;
then Z2 /\ Z <> {} by XBOOLE_0:def 7;
hence contradiction by A3; :: thesis: verum

end;

let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in Extend_Filter F,Z & Y2 in Extend_Filter F,Z implies Y1 /\ Y2 in Extend_Filter F,Z ) & ( Y1 in Extend_Filter F,Z & Y1 c= Y2 implies Y2 in Extend_Filter F,Z ) )
thus ( Y1 in Extend_Filter F,Z & Y2 in Extend_Filter F,Z implies Y1 /\ Y2 in Extend_Filter F,Z ) :: thesis: ( Y1 in Extend_Filter F,Z & Y1 c= Y2 implies Y2 in Extend_Filter F,Z )

proof

assume that
A4: Y1 in Extend_Filter F,Z and
A5: Y2 in Extend_Filter F,Z ; :: thesis: Y1 /\ Y2 in Extend_Filter F,Z
consider Y3 being Subset of X such that
A6: Y3 in F and
A7: Y3 /\ Z c= Y1 by A4, Th13;
consider Y4 being Subset of X such that
A8: Y4 in F and
A9: Y4 /\ Z c= Y2 by A5, Th13;
(Y3 /\ Z) /\ (Y4 /\ Z) = Y3 /\ (Z /\ (Y4 /\ Z)) by XBOOLE_1:16
.= Y3 /\ (Y4 /\ (Z /\ Z)) by XBOOLE_1:16
.= (Y3 /\ Y4) /\ Z by XBOOLE_1:16 ;
then A10: (Y3 /\ Y4) /\ Z c= Y1 /\ Y2 by A7, A9, XBOOLE_1:27;
Y3 /\ Y4 in F by A6, A8, Def1;
hence Y1 /\ Y2 in Extend_Filter F,Z by A10, Th13; :: thesis: verum

end;

thus ( Y1 in Extend_Filter F,Z & Y1 c= Y2 implies Y2 in Extend_Filter F,Z ) :: thesis: verum

proof

A11: X \ Z misses Z by XBOOLE_1:79;
(Y2 \/ (X \ Z)) /\ Z = (Y2 /\ Z) \/ ((X \ Z) /\ Z) by XBOOLE_1:23
.= (Y2 /\ Z) \/ {} by A11, XBOOLE_0:def 7
.= Y2 /\ Z ;
then A12: (Y2 \/ (X \ Z)) /\ Z c= Y2 by XBOOLE_1:17;
assume that
A13: Y1 in Extend_Filter F,Z and
A14: Y1 c= Y2 ; :: thesis: Y2 in Extend_Filter F,Z
consider Y3 being Subset of X such that
A15: Y3 in F and
A16: Y3 /\ Z c= Y1 by A13, Th13;
( Y3 = (Y3 /\ Z) \/ (Y3 \ Z) & Y3 \ Z c= X \ Z ) by XBOOLE_1:33, XBOOLE_1:51;
then A17: Y3 c= (Y3 /\ Z) \/ (X \ Z) by XBOOLE_1:9;
Y3 /\ Z c= Y2 by A14, A16, XBOOLE_1:1;
then (Y3 /\ Z) \/ (X \ Z) c= Y2 \/ (X \ Z) by XBOOLE_1:9;
then Y3 c= Y2 \/ (X \ Z) by A17, XBOOLE_1:1;
then Y2 \/ (X \ Z) in F by A15, Def1;
hence Y2 in Extend_Filter F,Z by A12, Th13; :: thesis: verum

end;

end;

thus F c= Extend_Filter F,Z :: thesis: verum

proof

let Y be set ; :: according to TARSKI:def 3 :: thesis: ( not Y in F or Y in Extend_Filter F,Z )
assume A18: Y in F ; :: thesis: Y in Extend_Filter F,Z
then reconsider Y = Y as Subset of X ;
Y /\ Z c= Y by XBOOLE_1:17;
hence Y in Extend_Filter F,Z by A18, Th13; :: thesis: verum

end;