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 )

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_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or ~ a <= b_{1} ) ) & ( for b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or ex b_{2} being Element of the carrier of L st

( X is_<=_than b_{2} & not b_{1} <= b_{2} ) or b_{1} = ~ a ) ) )

thus X is_<=_than ~ a by A6, Th9; :: thesis: ( ( for b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or ~ a <= b_{1} ) ) & ( for b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or ex b_{2} being Element of the carrier of L st

( X is_<=_than b_{2} & not b_{1} <= b_{2} ) or b_{1} = ~ a ) ) )

_{1} being Element of the carrier of L st

( X is_<=_than b_{1} & not c <= b_{1} ) or c = ~ a )

assume X is_<=_than c ; :: thesis: ( ex b_{1} being Element of the carrier of L st

( X is_<=_than b_{1} & not c <= b_{1} ) 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

( 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_inf_of X,L opp
; :: thesis: ex_sup_of X,Lassume
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

end;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_{1} being Element of the carrier of (L opp) holds

( not b_{1} is_<=_than X or b_{1} <= a ~ ) ) & ( for b_{1} being Element of the carrier of (L opp) holds

( not b_{1} is_<=_than X or ex b_{2} being Element of the carrier of (L opp) st

( b_{2} is_<=_than X & not b_{2} <= b_{1} ) or b_{1} = a ~ ) ) )

thus X is_>=_than a ~ by A1, Th8; :: thesis: ( ( for b_{1} being Element of the carrier of (L opp) holds

( not b_{1} is_<=_than X or b_{1} <= a ~ ) ) & ( for b_{1} being Element of the carrier of (L opp) holds

( not b_{1} is_<=_than X or ex b_{2} being Element of the carrier of (L opp) st

( b_{2} is_<=_than X & not b_{2} <= b_{1} ) or b_{1} = a ~ ) ) )

_{1} being Element of the carrier of (L opp) st

( b_{1} is_<=_than X & not b_{1} <= c ) or c = a ~ )

assume X is_>=_than c ; :: thesis: ( ex b_{1} being Element of the carrier of (L opp) st

( b_{1} is_<=_than X & not b_{1} <= 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 ~

end;( not b

( not b

( b

thus X is_>=_than a ~ by A1, Th8; :: thesis: ( ( for b

( not b

( not b

( b

hereby :: thesis: for b_{1} being Element of the carrier of (L opp) holds

( not b_{1} is_<=_than X or ex b_{2} being Element of the carrier of (L opp) st

( b_{2} is_<=_than X & not b_{2} <= b_{1} ) or b_{1} = a ~ )

let c be Element of (L opp); :: thesis: ( not c is_<=_than X or ex b( not b

( b

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;assume X is_>=_than b ; :: thesis: b <= a ~

then X is_<=_than ~ b by Th9;

hence b <= a ~ by Th2, A2; :: thesis: verum

( b

assume X is_>=_than c ; :: thesis: ( ex b

( b

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

hence
c = a ~
by A3, A4; :: thesis: verumb >= ~ 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;assume X is_<=_than b ; :: thesis: b >= ~ c

then X is_>=_than b ~ by Th8;

hence b >= ~ c by Th2, A5; :: thesis: verum

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

( not X is_<=_than b

( not X is_<=_than b

( X is_<=_than b

thus X is_<=_than ~ a by A6, Th9; :: thesis: ( ( for b

( not X is_<=_than b

( not X is_<=_than b

( X is_<=_than b

hereby :: thesis: for b_{1} being Element of the carrier of L holds

( not X is_<=_than b_{1} or ex b_{2} being Element of the carrier of L st

( X is_<=_than b_{2} & not b_{1} <= b_{2} ) or b_{1} = ~ a )

let c be Element of L; :: thesis: ( not X is_<=_than c or ex b( not X is_<=_than b

( X is_<=_than b

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;assume X is_<=_than b ; :: thesis: b >= ~ a

then X is_>=_than b ~ by Th8;

hence b >= ~ a by Th2, A7; :: thesis: verum

( X is_<=_than b

assume X is_<=_than c ; :: thesis: ( ex b

( X is_<=_than b

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 ~

hence
c = ~ a
by A8, A9; :: thesis: verumb <= 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;assume X is_>=_than b ; :: thesis: b <= c ~

then X is_<=_than ~ b by Th9;

hence b <= c ~ by Th2, A10; :: thesis: verum