theorem Th1: :: WAYBEL35:1

for L being 1-sorted
for C being trivial Subset of L
for R being Relation of the carrier of L holds C is strict_chain of R