let FT be non empty RelStr ; :: thesis: ( FT is filled & FT is symmetric & ( 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 ) implies FT is connected )
assume A1: ( FT is filled & FT is symmetric ) ; :: thesis: ( ex A, B being Subset of FT st
( [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed & not A meets B ) or FT is connected )
assume A2: 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 ; :: thesis: FT is connected
assume not FT is connected ; :: thesis: contradiction
then not [#] FT is connected ;
then consider P, Q being Subset of FT such that
A3: [#] FT = P \/ Q and
A4: P misses Q and
A5: P,Q are_separated and
A6: ( P <> {} FT & Q <> {} FT ) by A1, Th6;
( P is closed & Q is closed ) by A1, A3, A5, Th27;
hence contradiction by A2, A3, A4, A6; :: thesis: verum