ex p', q' being Element of H st p' <> q' 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