let H be non empty RelStr ; :: thesis: ( H is Heyting implies H is upper-bounded )
assume A1: H is Heyting ; :: thesis: H is upper-bounded
consider a being Element of H;
take x = a => a; :: according to YELLOW_0:def 5 :: thesis: the carrier of H is_<=_than x
let y be Element of H; :: according to LATTICE3:def 9 :: thesis: ( not y in the carrier of H or y <= x )
assume y in the carrier of H ; :: thesis: y <= x
a >= a "/\" y by A1, YELLOW_0:23;
hence y <= x by A1, Th70; :: thesis: verum