theorem :: WAYBEL35:11

for L being non empty antisymmetric lower-bounded RelStr
for R being auxiliary(iv) Relation of L
for C being strict_chain of R st C is maximal holds
Bottom L in C