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