consider p', q' being Element of H such that
A1: p' <> q' by STRUCT_0:def 10;
ex F being Filter of H st F in F_primeSet H by A1, Th23;
hence not F_primeSet H is empty ; :: thesis: verum