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)
let a be Element of H; :: thesis: Top H = a => (Top H)
a <= Top H by A1, YELLOW_0:45;
hence Top H = a => (Top H) by A1, Th69; :: thesis: verum