let L be RelStr ; :: thesis: for X being set holds
( ex_sup_of X,L iff ex_inf_of X,L opp )
let X be set ; :: thesis: ( ex_sup_of X,L iff ex_inf_of X,L opp )

hereby :: thesis: ( ex_inf_of X,L opp implies ex_sup_of X,L )

assume ex_sup_of X,L ; :: thesis: ex_inf_of X,L opp
then consider a being Element of L such that
A1: X is_<=_than a and
A2: for b being Element of L st X is_<=_than b holds
b >= a and
A3: for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
b >= c ) holds
c = a ;
thus ex_inf_of X,L opp :: thesis: verum

proof

take a ~ ; :: according to YELLOW_0:def 8 :: thesis: ( a ~ is_<=_than X & ( for b₁ being Element of the carrier of (L opp) holds
( not b₁ is_<=_than X or b₁ <= a ~ ) ) & ( for b₁ being Element of the carrier of (L opp) holds
( not b₁ is_<=_than X or ex b₂ being Element of the carrier of (L opp) st
( b₂ is_<=_than X & not b₂ <= b₁ ) or b₁ = a ~ ) ) )
thus X is_>=_than a ~ by A1, Th8; :: thesis: ( ( for b₁ being Element of the carrier of (L opp) holds
( not b₁ is_<=_than X or b₁ <= a ~ ) ) & ( for b₁ being Element of the carrier of (L opp) holds
( not b₁ is_<=_than X or ex b₂ being Element of the carrier of (L opp) st
( b₂ is_<=_than X & not b₂ <= b₁ ) or b₁ = a ~ ) ) )

hereby :: thesis: for b₁ being Element of the carrier of (L opp) holds
( not b₁ is_<=_than X or ex b₂ being Element of the carrier of (L opp) st
( b₂ is_<=_than X & not b₂ <= b₁ ) or b₁ = a ~ )

let b be Element of (L opp); :: thesis: ( X is_>=_than b implies b <= a ~ )
assume X is_>=_than b ; :: thesis: b <= a ~
then X is_<=_than ~ b by Th9;
hence b <= a ~ by Th2, A2; :: thesis: verum

end;

let c be Element of (L opp); :: thesis: ( not c is_<=_than X or ex b₁ being Element of the carrier of (L opp) st
( b₁ is_<=_than X & not b₁ <= c ) or c = a ~ )
assume X is_>=_than c ; :: thesis: ( ex b₁ being Element of the carrier of (L opp) st
( b₁ is_<=_than X & not b₁ <= c ) or c = a ~ )
then A4: X is_<=_than ~ c by Th9;
assume A5: for b being Element of (L opp) st X is_>=_than b holds
b <= c ; :: thesis: c = a ~

now :: thesis: for b being Element of L st X is_<=_than b holds
b >= ~ c

let b be Element of L; :: thesis: ( X is_<=_than b implies b >= ~ c )
assume X is_<=_than b ; :: thesis: b >= ~ c
then X is_>=_than b ~ by Th8;
hence b >= ~ c by Th2, A5; :: thesis: verum

end;

hence c = a ~ by A3, A4; :: thesis: verum

end;

end;

assume ex_inf_of X,L opp ; :: thesis: ex_sup_of X,L
then consider a being Element of (L opp) such that
A6: X is_>=_than a and
A7: for b being Element of (L opp) st X is_>=_than b holds
b <= a and
A8: for c being Element of (L opp) st X is_>=_than c & ( for b being Element of (L opp) st X is_>=_than b holds
b <= c ) holds
c = a ;
take ~ a ; :: according to YELLOW_0:def 7 :: thesis: ( X is_<=_than ~ a & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or ~ a <= b₁ ) ) & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or ex b₂ being Element of the carrier of L st
( X is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = ~ a ) ) )
thus X is_<=_than ~ a by A6, Th9; :: thesis: ( ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or ~ a <= b₁ ) ) & ( for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or ex b₂ being Element of the carrier of L st
( X is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = ~ a ) ) )

hereby :: thesis: for b₁ being Element of the carrier of L holds
( not X is_<=_than b₁ or ex b₂ being Element of the carrier of L st
( X is_<=_than b₂ & not b₁ <= b₂ ) or b₁ = ~ a )

let b be Element of L; :: thesis: ( X is_<=_than b implies b >= ~ a )
assume X is_<=_than b ; :: thesis: b >= ~ a
then X is_>=_than b ~ by Th8;
hence b >= ~ a by Th2, A7; :: thesis: verum

end;

let c be Element of L; :: thesis: ( not X is_<=_than c or ex b₁ being Element of the carrier of L st
( X is_<=_than b₁ & not c <= b₁ ) or c = ~ a )
assume X is_<=_than c ; :: thesis: ( ex b₁ being Element of the carrier of L st
( X is_<=_than b₁ & not c <= b₁ ) or c = ~ a )
then A9: X is_>=_than c ~ by Th8;
assume A10: for b being Element of L st X is_<=_than b holds
b >= c ; :: thesis: c = ~ a

now :: thesis: for b being Element of (L opp) st X is_>=_than b holds
b <= c ~

let b be Element of (L opp); :: thesis: ( X is_>=_than b implies b <= c ~ )
assume X is_>=_than b ; :: thesis: b <= c ~
then X is_<=_than ~ b by Th9;
hence b <= c ~ by Th2, A10; :: thesis: verum

end;

hence c = ~ a by A8, A9; :: thesis: verum