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 <> {} ;
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
.= 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;
end;
thus F c= Extend_Filter (F,Z) :: 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;