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 a => a ; :: according to YELLOW_0:def 5 :: thesis: the carrier of H is_<=_than a => a
let y be Element of H; :: according to LATTICE3:def 9 :: thesis: ( not y in the carrier of H or y <= a => a )
assume y in the carrier of H ; :: thesis: y <= a => a
a >= a "/\" y by A1, YELLOW_0:23;
hence y <= a => a by A1, Th70; :: thesis: verum