theorem :: ORDERS_1:24

for X being set
for O being Order of X st O is connected holds
O is being_linear-order ;