for L being non empty complete Poset
for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R st C is maximal holds
subrelstr C is complete