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:24;
then (Top H) "/\" ((Top H) => b) <= b by A1, Th70;
then A2: (Top H) => b <= b by A1, Th5;
(Top H) => b >= b by A1, Th75;
hence b = (Top H) => b by A1, A2, ORDERS_2:25; :: thesis: verum