let FT be non empty RelStr ; :: thesis: for A being Subset of FT st FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT ) holds
A is connected
let A be Subset of FT; :: thesis: ( FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT ) implies A is connected )
assume A1: FT is symmetric ; :: thesis: ( ex A2, B2 being Subset of FT st
( A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT & not B2 = {} FT ) or A is connected )
assume A2: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT ; :: thesis: A is connected
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 )

proof

let B, C be Subset of FT; :: thesis: ( A = B \/ C & B <> {} & C <> {} & B misses C implies ( B ^b meets C & B meets C ^b ) )
assume ( A = B \/ C & B <> {} & C <> {} & B misses C ) ; :: thesis: ( B ^b meets C & B meets C ^b )
then not B,C are_separated by A2;
then ( not B ^b misses C or not B misses C ^b ) by FINTOPO4:def 1;
hence ( B ^b meets C & B meets C ^b ) by A1, Th5; :: thesis: verum

end;

hence A is connected ; :: thesis: verum