let FT be non empty RelStr ; :: thesis: ( FT is connected implies for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds

B = {} FT )

assume FT is connected ; :: thesis: for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds

B = {} FT

then A1: [#] FT is connected ;

let A, B be Subset of FT; :: thesis: ( [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT implies B = {} FT )

assume that

A2: ( [#] FT = A \/ B & A misses B ) and

A3: A,B are_separated ; :: thesis: ( A = {} FT or B = {} FT )

A ^b misses B by A3, FINTOPO4:def 1;

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

B = {} FT )

assume FT is connected ; :: thesis: for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds

B = {} FT

then A1: [#] FT is connected ;

let A, B be Subset of FT; :: thesis: ( [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT implies B = {} FT )

assume that

A2: ( [#] FT = A \/ B & A misses B ) and

A3: A,B are_separated ; :: thesis: ( A = {} FT or B = {} FT )

A ^b misses B by A3, FINTOPO4:def 1;

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