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

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