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);

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

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

hence ex_sup_of X, subrelstr C by A1, Th7; :: thesis: verum

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;

end;