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 )

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

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

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