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