consider a, b being Element of L such that
A0: ( a in [#] L & b in [#] L & a <> b ) by SUBSET_1:45;
consider F being Filter of L such that
A1: F in F_primeSet L by OPENLATT:21, A0;
F_primeSet L c< PFilters L by PrimFil;
hence not StoneSpace L is empty by StoneDef, A1; :: thesis: verum