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 by Def1;
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, FIN_TOPO:def 16; :: thesis: verum