let H be non empty RelStr ; :: thesis: ( H is Heyting implies for a, b being Element of H holds
( Top H = a => b iff a <= b ) )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H holds
( Top H = a => b iff a <= b )
then A2: H is LATTICE ;
A3: H is upper-bounded by A1;
let a, b be Element of H; :: thesis: ( Top H = a => b iff a <= b )
A4: a "/\" (Top H) = (Top H) "/\" a by A2, LATTICE3:15
.= a by A2, A3, Th5 ;

hereby :: thesis: ( a <= b implies Top H = a => b )

assume Top H = a => b ; :: thesis: a <= b
then a => b >= Top H by A2, ORDERS_2:24;
hence a <= b by A1, A4, Th70; :: thesis: verum

end;

assume a <= b ; :: thesis: Top H = a => b
then A5: a => b >= Top H by A1, A4, Th70;
a => b <= Top H by A2, A3, YELLOW_0:45;
hence Top H = a => b by A2, A5, ORDERS_2:25; :: thesis: verum