let L be non empty RelStr ; 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 ; ( ( 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 )
; ( 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
; YELLOW_0:def 7 ex_sup_of Y,L
take
a
; YELLOW_0:def 7 ( 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; ( ( 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; 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; ( 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
; ( 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
; 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; verum