let n be Nat; :: thesis: for P being Subset of (TOP-REAL n) st P = REAL n holds
P is connected
let P be Subset of (TOP-REAL n); :: thesis: ( P = REAL n implies P is connected )
assume A1: P = REAL n ; :: thesis: P is connected
for p1, p2 being Point of (TOP-REAL n) st p1 in P & p2 in P holds
LSeg (p1,p2) c= P

proof

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( p1 in P & p2 in P implies LSeg (p1,p2) c= P )
assume that
p1 in P and
p2 in P ; :: thesis: LSeg (p1,p2) c= P
the carrier of (TOP-REAL n) = REAL n by EUCLID:22;
hence LSeg (p1,p2) c= P by A1; :: thesis: verum

end;

then P is convex by JORDAN1:def 1;
hence P is connected ; :: thesis: verum