let H be non empty RelStr ; ( H is Heyting & H is lower-bounded implies for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H } )
assume that
A1:
H is Heyting
and
A2:
H is lower-bounded
; for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }
let a be Element of H; 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }
set X = { x where x is Element of H : a "/\" x = Bottom H } ;
set Y = { x where x is Element of H : a "/\" x <= Bottom H } ;
A3:
{ x where x is Element of H : a "/\" x = Bottom H } = { x where x is Element of H : a "/\" x <= Bottom H }
A10:
ex_max_of { x where x is Element of H : a "/\" x = Bottom H } ,H
by A1, A3, Th62;
hence
ex_sup_of { x where x is Element of H : a "/\" x = Bottom H } ,H
; WAYBEL_1:def 7 ( 'not' a = "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) & "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H } )
'not' a is_>=_than { x where x is Element of H : a "/\" x = Bottom H }
hence
'not' a = "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H)
by A1, A8, YELLOW_0:30; "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H }
thus
"\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H }
by A10; verum