for A being non empty Poset
for S being Subset of A st the InternalRel of A |_2 S is being_linear-order holds
S is Chain of A