theorem :: ORDERS_2:10

for A being RelStr
for C being Chain of A
for S being Subset of A st S c= C holds
S is Chain of A