:: deftheorem defines connected FIN_TOPO:def 16 :
for FT being non empty RelStr
for IT being Subset of FT holds
( IT is connected iff for B, C being Subset of FT st IT = B \/ C & B <> {} & C <> {} & B misses C holds
B ^b meets C );