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) )
proof
defpred S1[ 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 : S1[Y] } ;
S1[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;
given Z2 being Subset of X such that A6: Z2 in F and
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
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;
hence Z1 in Extend_Filter (F,Z) ; :: thesis: verum