theorem Th5: :: WAYBEL35:5

for L being non empty antisymmetric lower-bounded RelStr
for R being auxiliary(iv) Relation of L
for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R