let FT be non empty RelStr ; :: thesis: for x being Point of FT holds {x} is connected
let x be Point of FT; :: thesis: {x} is connected
assume not {x} is connected ; :: thesis: contradiction
then consider P, Q being Subset of FT such that
A1: ( {x} = P \/ Q & P <> {} & Q <> {} & P misses Q & ( not P ^b meets Q or not P meets Q ^b ) ) by Th3;
P <> Q

proof

assume not P <> Q ; :: thesis: contradiction
then P /\ Q = P ;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

hence contradiction by A1, ZFMISC_1:44; :: thesis: verum