let L be non empty Poset; :: thesis:
let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis:
let C be non empty strict_chain of R; :: thesis:
let X be Subset of C; :: thesis:
assume that
A1: ex_sup_of X,L and
A2: C is maximal ; :: thesis:
set s = "\/" (X,L);

per cases ;

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

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

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 (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:

end;

end;