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

proof

given x being Element of (L opp) such that A1: x is_<=_than the carrier of (L opp) ; :: according to YELLOW_0:def 4 :: thesis: L is upper-bounded
take ~ x ; :: according to YELLOW_0:def 5 :: thesis: the carrier of L is_<=_than ~ x
thus the carrier of L is_<=_than ~ x by A1, Th9; :: thesis: verum

end;

given x being Element of L such that A2: x is_>=_than the carrier of L ; :: according to YELLOW_0:def 5 :: thesis: L opp is lower-bounded
take x ~ ; :: according to YELLOW_0:def 4 :: thesis: x ~ is_<=_than the carrier of (L opp)
thus x ~ is_<=_than the carrier of (L opp) by A2, Th8; :: thesis: verum