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
then A2: H is LATTICE ;
let a be Element of H; :: thesis: Top H = a => a
a >= a "/\" (Top H) by A2, YELLOW_0:23;
then A3: Top H <= a => a by A1, Th70;
H is upper-bounded by A1;
then Top H >= a => a by A2, YELLOW_0:45;
hence Top H = a => a by A2, A3, ORDERS_2:25; :: thesis: verum