:: deftheorem defines disconnected ORDERS_3:def 2 :
for P being RelStr
for IT being Subset of P holds
( IT is disconnected iff ex A, B being Subset of P st
( A <> {} & B <> {} & IT = A \/ B & A misses B & the InternalRel of P = ( the InternalRel of P |_2 A) \/ ( the InternalRel of P |_2 B) ) );