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 and

A2: P <> {} and

A3: Q <> {} and

A4: P misses Q and

( not P ^b meets Q or not P meets Q ^b ) ;

P <> Q by A2, A4;

hence contradiction by A1, A2, A3, ZFMISC_1:38; :: thesis: verum

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 and

A2: P <> {} and

A3: Q <> {} and

A4: P misses Q and

( not P ^b meets Q or not P meets Q ^b ) ;

P <> Q by A2, A4;

hence contradiction by A1, A2, A3, ZFMISC_1:38; :: thesis: verum