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 A2: ( A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated ) ; :: thesis: ( A2 = {} FT or B2 = {} FT )
then ( A2 ^b misses B2 & A2 misses B2 ^b ) by FINTOPO4:def 1;
hence ( A2 = {} FT or B2 = {} FT ) by A1, A2, FIN_TOPO:def 18; :: thesis: verum