let L be non empty RelStr ; :: thesis: ( L is complete implies L is bounded )
assume A1: for X being set ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) ) ; :: according to LATTICE3:def 12 :: thesis: L is bounded
then consider a0 being Element of L such that
{} is_<=_than a0 and
A2: for b being Element of L st {} is_<=_than b holds
a0 <= b ;
consider a1 being Element of L such that
A3: the carrier of L is_<=_than a1 and
for b being Element of L st the carrier of L is_<=_than b holds
a1 <= b by A1;
reconsider a0 = a0, a1 = a1 as Element of L ;
hereby :: according to YELLOW_0:def 4,YELLOW_0:def 6 :: thesis: L is upper-bounded
take a0 = a0; :: thesis: a0 is_<=_than the carrier of L
thus a0 is_<=_than the carrier of L by A2, Th6; :: thesis: verum
end;
take a1 ; :: according to YELLOW_0:def 5 :: thesis: a1 is_>=_than the carrier of L
thus a1 is_>=_than the carrier of L by A3; :: thesis: verum