let FT be non empty RelStr ; :: thesis: ( FT is connected implies for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds
A meets B )
assume A1: [#] FT is connected ; :: according to FINTOPO6:def 1 :: thesis: for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds
A meets B
given A, B being Subset of FT such that A2: ( [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed & A misses B ) ; :: thesis: contradiction
thus contradiction by A1, A2; :: thesis: verum