let L be RelStr ; :: thesis: ( L is empty implies L is bounded )
assume A1: L is empty ; :: thesis: L is bounded
set x = the Element of L;
thus L is lower-bounded :: according to YELLOW_0:def 6 :: thesis: L is upper-bounded
proof
take the Element of L ; :: according to YELLOW_0:def 4 :: thesis: the Element of L 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 the Element of L <= a )
assume a in the carrier of L ; :: thesis: the Element of L <= a
hence the Element of L <= a by A1; :: thesis: verum
end;
take the Element of L ; :: according to YELLOW_0:def 5 :: thesis: the carrier of L is_<=_than the Element of L
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in the carrier of L or a <= the Element of L )
assume a in the carrier of L ; :: thesis: a <= the Element of L
hence a <= the Element of L by A1; :: thesis: verum