let H be non empty RelStr ; :: thesis: ( H is Heyting implies for a being Element of H holds Top H = a => a )
assume A1: H is Heyting ; :: thesis: for a being Element of H holds Top H = a => a
let a be Element of H; :: thesis: Top H = a => a
a >= a "/\" (Top H) by A1, YELLOW_0:23;
then A2: Top H <= a => a by A1, Th67;
Top H >= a => a by A1, YELLOW_0:45;
hence Top H = a => a by A1, A2, ORDERS_2:2; :: thesis: verum