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

proof

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

end;

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