for L being non empty antisymmetric lower-bounded RelStr
for x being Element of L
for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R