let H be non empty RelStr ; :: thesis: ( H is Heyting implies for a being Element of H holds Top H = a => (Top H) )
assume A1: H is Heyting ; :: thesis: for a being Element of H holds Top H = a => (Top H)
then A2: H is LATTICE ;
let a be Element of H; :: thesis: Top H = a => (Top H)
H is upper-bounded by A1;
then a <= Top H by A2, YELLOW_0:45;
hence Top H = a => (Top H) by A1, Th72; :: thesis: verum