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 )

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

hence
A is connected
; :: thesis: verum
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;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