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