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
then A2: H is LATTICE ;
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 A2, YELLOW_0:23;
hence x >= y by A1, Th70; :: thesis: verum