ex p9, q9 being Element of H st p9 <> q9 by STRUCT_0:def 10;
then ex F being Filter of H st F in F_primeSet H by Th23;
hence not F_primeSet H is empty ; :: thesis: verum