let X be non empty set ; :: thesis:
let Z be Subset of X; :: thesis:
let F be Filter of X; :: thesis:
assume A1: for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ; :: thesis:
thus Z in Extend_Filter F,Z :: thesis:

ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z )

( X in F & X /\ Z c= Z ) by Th5, XBOOLE_1:17;
hence ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z ) ; :: thesis:

end;

hence Z in Extend_Filter F,Z by Th13; :: thesis:

end;

thus Extend_Filter F,Z is Filter of X :: thesis:

thus not {} in Extend_Filter F,Z :: according to CARD_FIL:def 1 :: thesis:

assume {} in Extend_Filter F,Z ; :: thesis:
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:

end;

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

assume A4: ( Y1 in Extend_Filter F,Z & Y2 in Extend_Filter F,Z ) ; :: thesis:
then consider Y3 being Subset of X such that
A5: Y3 in F and
A6: Y3 /\ Z c= Y1 by Th13;
consider Y4 being Subset of X such that
A7: Y4 in F and
A8: Y4 /\ Z c= Y2 by A4, Th13;
A9: Y3 /\ Y4 in F by A5, A7, Def1;
(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 (Y3 /\ Y4) /\ Z c= Y1 /\ Y2 by A6, A8, XBOOLE_1:27;
hence Y1 /\ Y2 in Extend_Filter F,Z by A9, Th13; :: thesis:

end;

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

assume A10: ( Y1 in Extend_Filter F,Z & Y1 c= Y2 ) ; :: thesis:
then consider Y3 being Subset of X such that
A11: Y3 in F and
A12: Y3 /\ Z c= Y1 by Th13;
A13: Y3 /\ Z c= Y2 by A10, A12, XBOOLE_1:1;
Y3 c= Y2 \/ (X \ Z)

A14: Y3 = (Y3 /\ Z) \/ (Y3 \ Z) by XBOOLE_1:51;
Y3 \ Z c= X \ Z by XBOOLE_1:33;
then A15: Y3 c= (Y3 /\ Z) \/ (X \ Z) by A14, XBOOLE_1:9;
(Y3 /\ Z) \/ (X \ Z) c= Y2 \/ (X \ Z) by A13, XBOOLE_1:9;
hence Y3 c= Y2 \/ (X \ Z) by A15, XBOOLE_1:1; :: thesis:

end;

then A16: Y2 \/ (X \ Z) in F by A11, Def1;
A17: X \ Z misses Z by XBOOLE_1:79;
(Y2 \/ (X \ Z)) /\ Z = (Y2 /\ Z) \/ ((X \ Z) /\ Z) by XBOOLE_1:23
.= (Y2 /\ Z) \/ {} by A17, XBOOLE_0:def 7
.= Y2 /\ Z ;
then (Y2 \/ (X \ Z)) /\ Z c= Y2 by XBOOLE_1:17;
hence Y2 in Extend_Filter F,Z by A16, Th13; :: thesis:

end;

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

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

end;