a in <.a.) ;
then <.a.) in { F where F is Filter of L : a in F } ;
hence not SF_have a is empty ; :: thesis: verum