let L be RelStr ; :: thesis: ( L is bounded iff L opp is bounded )
thus ( L is bounded implies L opp is bounded ) :: thesis: ( L opp is bounded implies L is bounded )

proof

assume ( L is lower-bounded & L is upper-bounded ) ; :: according to YELLOW_0:def 6 :: thesis: L opp is bounded
hence ( L opp is lower-bounded & L opp is upper-bounded ) by Th30, Th31; :: according to YELLOW_0:def 6 :: thesis: verum

end;

assume ( L opp is lower-bounded & L opp is upper-bounded ) ; :: according to YELLOW_0:def 6 :: thesis: L is bounded
hence ( L is lower-bounded & L is upper-bounded ) by Th30, Th31; :: according to YELLOW_0:def 6 :: thesis: verum