let L be RelStr ; :: thesis: ( L is empty implies L is bounded )
assume A1: L is empty ; :: thesis: L is bounded
consider x being Element of L;
thus L is lower-bounded :: according to YELLOW_0:def 6 :: thesis: L is upper-bounded

proof

take x ; :: according to YELLOW_0:def 4 :: thesis: x is_<=_than the carrier of L
let a be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not a in the carrier of L or x <= a )
assume a in the carrier of L ; :: thesis: x <= a
hence x <= a by A1; :: thesis: verum

end;

take x ; :: according to YELLOW_0:def 5 :: thesis: the carrier of L is_<=_than x
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in the carrier of L or a <= x )
assume a in the carrier of L ; :: thesis: a <= x
hence a <= x by A1; :: thesis: verum