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 )

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

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 such that A2:
x is_>=_than the carrier of L
; :: according to YELLOW_0:def 5 :: thesis: L opp is lower-bounded
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;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

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