let X be non empty set ; :: thesis: for Z being Subset of X

for F being Filter of X

for Z1 being Subset of X holds

( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 ) )

let Z be Subset of X; :: thesis: for F being Filter of X

for Z1 being Subset of X holds

( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 ) )

let F be Filter of X; :: thesis: for Z1 being Subset of X holds

( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 ) )

let Z1 be Subset of X; :: thesis: ( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 ) )

thus ( Z1 in Extend_Filter (F,Z) implies ex Z2 being Subset of X st

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

( Z2 in F & Z2 /\ Z c= Z1 ) implies Z1 in Extend_Filter (F,Z) )

A7: Z2 /\ Z c= Z1 ; :: thesis: Z1 in Extend_Filter (F,Z)

ex Y2 being Subset of X st

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Z1 )

for F being Filter of X

for Z1 being Subset of X holds

( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 ) )

let Z be Subset of X; :: thesis: for F being Filter of X

for Z1 being Subset of X holds

( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 ) )

let F be Filter of X; :: thesis: for Z1 being Subset of X holds

( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 ) )

let Z1 be Subset of X; :: thesis: ( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 ) )

thus ( Z1 in Extend_Filter (F,Z) implies ex Z2 being Subset of X st

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

( Z2 in F & Z2 /\ Z c= Z1 ) implies Z1 in Extend_Filter (F,Z) )

proof

given Z2 being Subset of X such that A6:
Z2 in F
and
defpred S_{1}[ set ] means ex Y2 being Subset of X st

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= $1 );

assume Z1 in Extend_Filter (F,Z) ; :: thesis: ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 )

then A1: Z1 in { Y where Y is Subset of X : S_{1}[Y] }
;

S_{1}[Z1]
from CARD_FIL:sch 1(A1);

then consider Y2 being Subset of X such that

A2: Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } and

A3: Y2 c= Z1 ;

consider Y3 being Subset of X such that

A4: Y2 = Y3 /\ Z and

A5: Y3 in F by A2;

take Y3 ; :: thesis: ( Y3 in F & Y3 /\ Z c= Z1 )

thus Y3 in F by A5; :: thesis: Y3 /\ Z c= Z1

thus Y3 /\ Z c= Z1 by A3, A4; :: thesis: verum

end;( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= $1 );

assume Z1 in Extend_Filter (F,Z) ; :: thesis: ex Z2 being Subset of X st

( Z2 in F & Z2 /\ Z c= Z1 )

then A1: Z1 in { Y where Y is Subset of X : S

S

then consider Y2 being Subset of X such that

A2: Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } and

A3: Y2 c= Z1 ;

consider Y3 being Subset of X such that

A4: Y2 = Y3 /\ Z and

A5: Y3 in F by A2;

take Y3 ; :: thesis: ( Y3 in F & Y3 /\ Z c= Z1 )

thus Y3 in F by A5; :: thesis: Y3 /\ Z c= Z1

thus Y3 /\ Z c= Z1 by A3, A4; :: thesis: verum

A7: Z2 /\ Z c= Z1 ; :: thesis: Z1 in Extend_Filter (F,Z)

ex Y2 being Subset of X st

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Z1 )

proof

hence
Z1 in Extend_Filter (F,Z)
; :: thesis: verum
take
Z2 /\ Z
; :: thesis: ( Z2 /\ Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Z2 /\ Z c= Z1 )

thus Z2 /\ Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } by A6; :: thesis: Z2 /\ Z c= Z1

thus Z2 /\ Z c= Z1 by A7; :: thesis: verum

end;thus Z2 /\ Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } by A6; :: thesis: Z2 /\ Z c= Z1

thus Z2 /\ Z c= Z1 by A7; :: thesis: verum