let H be non empty RelStr ; ( H is Heyting implies for a, b being Element of H holds
( Top H = a => b iff a <= b ) )
assume A1:
H is Heyting
; for a, b being Element of H holds
( Top H = a => b iff a <= b )
let a, b be Element of H; ( Top H = a => b iff a <= b )
A2: a "/\" (Top H) =
(Top H) "/\" a
by A1, LATTICE3:15
.=
a
by A1, Th4
;
hereby ( a <= b implies Top H = a => b )
end;
assume
a <= b
; Top H = a => b
then A3:
a => b >= Top H
by A1, A2, Th67;
a => b <= Top H
by A1, YELLOW_0:45;
hence
Top H = a => b
by A1, A3, ORDERS_2:2; verum