theorem :: ORDERS_2:49

for A being non empty Poset
for S being Subset of A st the InternalRel of A linearly_orders S holds
S is Chain of A by ORDERS_1:7, Def7;