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:
set s = "\/" (X,L);
per cases ( "\/" (X,L) in C or not "\/" (X,L) in C ) ;
suppose "\/" (X,L) in C ; :: thesis:
hence ex_sup_of X, subrelstr C by ; :: thesis: verum
end;
suppose not "\/" (X,L) in C ; :: thesis:
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 () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () 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;
end;