let L be non empty RelStr ; :: thesis: for X, Y being set st ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L holds
ex_sup_of Y,L
let X, Y be set ; :: thesis: ( ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L implies ex_sup_of Y,L )
assume A1: for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ; :: thesis: ( not ex_sup_of X,L or ex_sup_of Y,L )
given a being Element of L such that A2: X is_<=_than a and
A3: for b being Element of L st X is_<=_than b holds
a <= b and
A4: for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
c <= b ) holds
c = a ; :: according to YELLOW_0:def 7 :: thesis: ex_sup_of Y,L
take a ; :: according to YELLOW_0:def 7 :: thesis: ( Y is_<=_than a & ( for b being Element of L st Y is_<=_than b holds
b >= a ) & ( 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 ) )
thus Y is_<=_than a by A1, A2; :: thesis: ( ( for b being Element of L st Y is_<=_than b holds
b >= a ) & ( 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 ) )
thus for b being Element of L st Y is_<=_than b holds
a <= b by A1, A3; :: thesis: 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
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 A5: Y is_<=_than c ; :: thesis: ( ex b being Element of L st
( Y is_<=_than b & not b >= c ) or c = a )
assume A6: for b being Element of L st Y is_<=_than b holds
c <= b ; :: thesis: c = a
A7: for b being Element of L st X is_<=_than b holds
c <= b by A1, A6;
X is_<=_than c by A1, A5;
hence c = a by A4, A7; :: thesis: verum