theorem
for
L being non
empty Poset 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_inf_of (uparrow ("\/" (X,L))) /\ C,
L &
ex_sup_of X,
L &
C is
maximal holds
(
"\/" (
X,
(subrelstr C))
= "/\" (
((uparrow ("\/" (X,L))) /\ C),
L) & ( not
"\/" (
X,
L)
in C implies
"\/" (
X,
L)
< "/\" (
((uparrow ("\/" (X,L))) /\ C),
L) ) )