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 )
let a, b be Element of H; :: thesis: ( Top H = a => b iff a <= b )
A2: a "/\" (Top H) = (Top H) "/\" a by A1, LATTICE3:15
.= a by A1, Th4 ;
hereby :: thesis: ( a <= b implies Top H = a => b )
assume Top H = a => b ; :: thesis: a <= b
then a => b >= Top H by A1, ORDERS_2:1;
hence a <= b by A1, A2, Th67; :: thesis: verum
end;
assume a <= b ; :: thesis: 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; :: thesis: verum