let L be RelStr ; :: thesis: ( L is lower-bounded & L is upper-bounded implies L is bounded )
assume ( L is lower-bounded & L is upper-bounded ) ; :: thesis: L is bounded
hence ( L is lower-bounded & L is upper-bounded ) ; :: according to YELLOW_0:def 6 :: thesis: verum