let H be non empty RelStr ; ( H is Heyting & H is lower-bounded implies ( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H ) )
assume that
A1:
H is Heyting
and
A2:
H is lower-bounded
; ( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H )
(Top H) => (Bottom H) <= (Top H) => (Bottom H)
by A1, ORDERS_2:1;
then A3:
Bottom H >= (Top H) "/\" ('not' (Top H))
by A1, Th67;
Bottom H >= (Bottom H) "/\" (Top H)
by A1, YELLOW_0:23;
then A4:
Top H <= (Bottom H) => (Bottom H)
by A1, Th67;
Bottom H <= (Top H) "/\" ('not' (Top H))
by A1, A2, YELLOW_0:44;
then A5:
Bottom H = (Top H) "/\" ('not' (Top H))
by A1, A3, ORDERS_2:2;
'not' (Bottom H) <= Top H
by A1, YELLOW_0:45;
hence
Top H = 'not' (Bottom H)
by A1, A4, ORDERS_2:2; 'not' (Top H) = Bottom H
'not' (Top H) <= Top H
by A1, YELLOW_0:45;
hence 'not' (Top H) =
('not' (Top H)) "/\" (Top H)
by A1, YELLOW_0:25
.=
Bottom H
by A1, A5, LATTICE3:15
;
verum