let L be non empty Poset; :: thesis: for R being auxiliary(i) auxiliary(ii) Relation of L

for C being non empty strict_chain of R

for X being Subset of C st ex_sup_of X,L & C is maximal holds

ex_sup_of X, subrelstr C

let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: for C being non empty strict_chain of R

for X being Subset of C st ex_sup_of X,L & C is maximal holds

ex_sup_of X, subrelstr C

let C be non empty strict_chain of R; :: thesis: for X being Subset of C st ex_sup_of X,L & C is maximal holds

ex_sup_of X, subrelstr C

let X be Subset of C; :: thesis: ( ex_sup_of X,L & C is maximal implies ex_sup_of X, subrelstr C )

assume that

A1: ex_sup_of X,L and

A2: C is maximal ; :: thesis: ex_sup_of X, subrelstr C

set s = "\/" (X,L);

for C being non empty strict_chain of R

for X being Subset of C st ex_sup_of X,L & C is maximal holds

ex_sup_of X, subrelstr C

let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: for C being non empty strict_chain of R

for X being Subset of C st ex_sup_of X,L & C is maximal holds

ex_sup_of X, subrelstr C

let C be non empty strict_chain of R; :: thesis: for X being Subset of C st ex_sup_of X,L & C is maximal holds

ex_sup_of X, subrelstr C

let X be Subset of C; :: thesis: ( ex_sup_of X,L & C is maximal implies ex_sup_of X, subrelstr C )

assume that

A1: ex_sup_of X,L and

A2: C is maximal ; :: thesis: ex_sup_of X, subrelstr C

set s = "\/" (X,L);

per cases
( "\/" (X,L) in C or not "\/" (X,L) in C )
;

end;

suppose
not "\/" (X,L) in C
; :: thesis: ex_sup_of X, subrelstr C

then
ex cs being Element of L st

( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a ) ) ) by A1, A2, Lm2;

hence ex_sup_of X, subrelstr C by YELLOW_0:15; :: thesis: verum

end;( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a ) ) ) by A1, A2, Lm2;

hence ex_sup_of X, subrelstr C by YELLOW_0:15; :: thesis: verum