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)

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
F c= Extend_Filter (F,Z)
:: thesis: verum
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) ) )

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) )

end;( ( 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

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) ) )
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 <> {} ;

hence contradiction by A3; :: thesis: verum

end;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 <> {} ;

hence contradiction by A3; :: thesis: verum

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

thus
( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) )
:: thesis: verum
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;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

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

.= 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;

then (Y3 /\ Z) \/ (X \ Z) c= Y2 \/ (X \ Z) by XBOOLE_1:9;

then Y3 c= Y2 \/ (X \ Z) by A17;

then Y2 \/ (X \ Z) in F by A15, Def1;

hence Y2 in Extend_Filter (F,Z) by A12, Th13; :: thesis: verum

end;(Y2 \/ (X \ Z)) /\ Z = (Y2 /\ Z) \/ ((X \ Z) /\ Z) by XBOOLE_1:23

.= (Y2 /\ Z) \/ {} by A11

.= 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;

then (Y3 /\ Z) \/ (X \ Z) c= Y2 \/ (X \ Z) by XBOOLE_1:9;

then Y3 c= Y2 \/ (X \ Z) by A17;

then Y2 \/ (X \ Z) in F by A15, Def1;

hence Y2 in Extend_Filter (F,Z) by A12, Th13; :: thesis: verum

proof

let Y be object ; :: 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;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