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