let X be non empty TopSpace; :: thesis: ( X is locally_connected implies for S being Subset of X st S is a_component holds

S is open )

assume A1: X is locally_connected ; :: thesis: for S being Subset of X st S is a_component holds

S is open

let S be Subset of X; :: thesis: ( S is a_component implies S is open )

assume A2: S is a_component ; :: thesis: S is open

then Int S = S by XBOOLE_0:def 10;

hence S is open ; :: thesis: verum

S is open )

assume A1: X is locally_connected ; :: thesis: for S being Subset of X st S is a_component holds

S is open

let S be Subset of X; :: thesis: ( S is a_component implies S is open )

assume A2: S is a_component ; :: thesis: S is open

now :: thesis: for p being object st p in S holds

p in Int S

then
( Int S c= S & S c= Int S )
by TOPS_1:16;p in Int S

let p be object ; :: thesis: ( p in S implies p in Int S )

assume A3: p in S ; :: thesis: p in Int S

then reconsider x = p as Point of X ;

A4: [#] X is a_neighborhood of x by Th3;

( X is_locally_connected_in x & S is_a_component_of [#] X ) by A1, A2, Th11;

then S is a_neighborhood of x by A3, A4, Th13;

hence p in Int S by Def1; :: thesis: verum

end;assume A3: p in S ; :: thesis: p in Int S

then reconsider x = p as Point of X ;

A4: [#] X is a_neighborhood of x by Th3;

( X is_locally_connected_in x & S is_a_component_of [#] X ) by A1, A2, Th11;

then S is a_neighborhood of x by A3, A4, Th13;

hence p in Int S by Def1; :: thesis: verum

then Int S = S by XBOOLE_0:def 10;

hence S is open ; :: thesis: verum