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

hereby :: thesis: ( ( for Y being set holds ex_inf_of Y,L ) implies for X being set holds ex_sup_of X,L )

assume A1: for X being set holds ex_sup_of X,L ; :: thesis: for Y being set holds ex_inf_of Y,L
let Y be set ; :: thesis: ex_inf_of Y,L
set X = { x where x is Element of L : x is_<=_than Y } ;
ex_sup_of { x where x is Element of L : x is_<=_than Y } ,L by A1;
then consider a being Element of L such that
A2: { x where x is Element of L : x is_<=_than Y } is_<=_than a and
A3: for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds
b >= a and
A4: for c being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than c & ( for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds
b >= c ) holds
c = a by YELLOW_0:def 7;
A5: a is_<=_than Y

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in Y or a <= b )
assume A6: b in Y ; :: thesis: a <= b
b is_>=_than { x where x is Element of L : x is_<=_than Y }

proof

let c be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c in { x where x is Element of L : x is_<=_than Y } or c <= b )
assume c in { x where x is Element of L : x is_<=_than Y } ; :: thesis: c <= b
then ex x being Element of L st
( c = x & x is_<=_than Y ) ;
hence c <= b by A6; :: thesis: verum

end;

hence a <= b by A3; :: thesis: verum

end;

A7: for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds
b <= c ) holds
c = a

proof

let c be Element of L; :: thesis: ( Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds
b <= c ) implies c = a )
assume that
A8: Y is_>=_than c and
A9: for b being Element of L st Y is_>=_than b holds
b <= c ; :: thesis: c = a
A10: for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds
b >= c

proof

let b be Element of L; :: thesis: ( { x where x is Element of L : x is_<=_than Y } is_<=_than b implies b >= c )
assume A11: { x where x is Element of L : x is_<=_than Y } is_<=_than b ; :: thesis: b >= c
c in { x where x is Element of L : x is_<=_than Y } by A8;
hence b >= c by A11; :: thesis: verum

end;

{ x where x is Element of L : x is_<=_than Y } is_<=_than c

proof

let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in { x where x is Element of L : x is_<=_than Y } or b <= c )
assume b in { x where x is Element of L : x is_<=_than Y } ; :: thesis: b <= c
then ex x being Element of L st
( b = x & x is_<=_than Y ) ;
hence b <= c by A9; :: thesis: verum

end;

hence c = a by A4, A10; :: thesis: verum

end;

for b being Element of L st Y is_>=_than b holds
a >= b

proof

let b be Element of L; :: thesis: ( Y is_>=_than b implies a >= b )
assume b is_<=_than Y ; :: thesis: a >= b
then b in { x where x is Element of L : x is_<=_than Y } ;
hence a >= b by A2; :: thesis: verum

end;

hence ex_inf_of Y,L by A5, A7, YELLOW_0:def 8; :: thesis: verum

end;

assume A12: for Y being set holds ex_inf_of Y,L ; :: thesis: for X being set holds ex_sup_of X,L
let X be set ; :: thesis: ex_sup_of X,L
set Y = { y where y is Element of L : X is_<=_than y } ;
ex_inf_of { y where y is Element of L : X is_<=_than y } ,L by A12;
then consider a being Element of L such that
A13: { y where y is Element of L : X is_<=_than y } is_>=_than a and
A14: for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds
b <= a and
A15: for c being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than c & ( for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds
b <= c ) holds
c = a by YELLOW_0:def 8;
A16: X is_<=_than a

proof

let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in X or b <= a )
assume A17: b in X ; :: thesis: b <= a
b is_<=_than { y where y is Element of L : X is_<=_than y }

proof

let c be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not c in { y where y is Element of L : X is_<=_than y } or b <= c )
assume c in { y where y is Element of L : X is_<=_than y } ; :: thesis: b <= c
then ex y being Element of L st
( c = y & X is_<=_than y ) ;
hence b <= c by A17; :: thesis: verum

end;

hence b <= a by A14; :: thesis: verum

end;

A18: 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

proof

let c be Element of L; :: thesis: ( X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
b >= c ) implies c = a )
assume that
A19: X is_<=_than c and
A20: for b being Element of L st X is_<=_than b holds
b >= c ; :: thesis: c = a
A21: for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds
b <= c

proof

let b be Element of L; :: thesis: ( { y where y is Element of L : X is_<=_than y } is_>=_than b implies b <= c )
assume A22: { y where y is Element of L : X is_<=_than y } is_>=_than b ; :: thesis: b <= c
c in { y where y is Element of L : X is_<=_than y } by A19;
hence b <= c by A22; :: thesis: verum

end;

{ y where y is Element of L : X is_<=_than y } is_>=_than c

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in { y where y is Element of L : X is_<=_than y } or c <= b )
assume b in { y where y is Element of L : X is_<=_than y } ; :: thesis: c <= b
then ex x being Element of L st
( b = x & x is_>=_than X ) ;
hence c <= b by A20; :: thesis: verum

end;

hence c = a by A15, A21; :: thesis: verum

end;

for b being Element of L st X is_<=_than b holds
a <= b

proof

let b be Element of L; :: thesis: ( X is_<=_than b implies a <= b )
assume X is_<=_than b ; :: thesis: a <= b
then b in { y where y is Element of L : X is_<=_than y } ;
hence a <= b by A13; :: thesis: verum

end;

hence ex_sup_of X,L by A16, A18, YELLOW_0:def 7; :: thesis: verum