let FT be non empty RelStr ; :: thesis: for A being Subset of FT st A is connected holds

for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds

B2 = {} FT

let A be Subset of FT; :: thesis: ( A is connected implies for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds

B2 = {} FT )

assume A1: A is connected ; :: thesis: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds

B2 = {} FT

let A2, B2 be Subset of FT; :: thesis: ( A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT implies B2 = {} FT )

assume that

A2: ( A = A2 \/ B2 & A2 misses B2 ) and

A3: A2,B2 are_separated ; :: thesis: ( A2 = {} FT or B2 = {} FT )

A2 ^b misses B2 by A3, FINTOPO4:def 1;

hence ( A2 = {} FT or B2 = {} FT ) by A1, A2; :: thesis: verum

for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds

B2 = {} FT

let A be Subset of FT; :: thesis: ( A is connected implies for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds

B2 = {} FT )

assume A1: A is connected ; :: thesis: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds

B2 = {} FT

let A2, B2 be Subset of FT; :: thesis: ( A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT implies B2 = {} FT )

assume that

A2: ( A = A2 \/ B2 & A2 misses B2 ) and

A3: A2,B2 are_separated ; :: thesis: ( A2 = {} FT or B2 = {} FT )

A2 ^b misses B2 by A3, FINTOPO4:def 1;

hence ( A2 = {} FT or B2 = {} FT ) by A1, A2; :: thesis: verum