let FT be non empty RelStr ; :: thesis: for A being Subset of FT st ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
( B ^b meets C & B meets C ^b ) ) holds
A is connected
let A be Subset of FT; :: thesis: ( ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
( B ^b meets C & B meets C ^b ) ) implies A is connected )
assume for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
( B ^b meets C & B meets C ^b ) ; :: thesis: A is connected
then for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
B ^b meets C ;
hence A is connected by FIN_TOPO:def 18; :: thesis: verum