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 b1 being Element of the carrier of (L opp) holds
( not b1 is_<=_than X or b1 <= a ~ ) ) & ( for b1 being Element of the carrier of (L opp) holds
( not b1 is_<=_than X or ex b2 being Element of the carrier of (L opp) st
( b2 is_<=_than X & not b2 <= b1 ) or b1 = a ~ ) ) )

thus X is_>=_than a ~ by ; :: thesis: ( ( for b1 being Element of the carrier of (L opp) holds
( not b1 is_<=_than X or b1 <= a ~ ) ) & ( for b1 being Element of the carrier of (L opp) holds
( not b1 is_<=_than X or ex b2 being Element of the carrier of (L opp) st
( b2 is_<=_than X & not b2 <= b1 ) or b1 = a ~ ) ) )

hereby :: thesis: for b1 being Element of the carrier of (L opp) holds
( not b1 is_<=_than X or ex b2 being Element of the carrier of (L opp) st
( b2 is_<=_than X & not b2 <= b1 ) or b1 = 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 ; :: thesis: verum
end;
let c be Element of (L opp); :: thesis: ( not c is_<=_than X or ex b1 being Element of the carrier of (L opp) st
( b1 is_<=_than X & not b1 <= c ) or c = a ~ )

assume X is_>=_than c ; :: thesis: ( ex b1 being Element of the carrier of (L opp) st
( b1 is_<=_than X & not b1 <= 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 ; :: 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 b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ~ a <= b1 ) ) & ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ex b2 being Element of the carrier of L st
( X is_<=_than b2 & not b1 <= b2 ) or b1 = ~ a ) ) )

thus X is_<=_than ~ a by ; :: thesis: ( ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ~ a <= b1 ) ) & ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ex b2 being Element of the carrier of L st
( X is_<=_than b2 & not b1 <= b2 ) or b1 = ~ a ) ) )

hereby :: thesis: for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ex b2 being Element of the carrier of L st
( X is_<=_than b2 & not b1 <= b2 ) or b1 = ~ 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 ; :: thesis: verum
end;
let c be Element of L; :: thesis: ( not X is_<=_than c or ex b1 being Element of the carrier of L st
( X is_<=_than b1 & not c <= b1 ) or c = ~ a )

assume X is_<=_than c ; :: thesis: ( ex b1 being Element of the carrier of L st
( X is_<=_than b1 & not c <= b1 ) 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 ; :: thesis: verum
end;
hence c = ~ a by A8, A9; :: thesis: verum