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