for X being non empty set
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 ) )