let X be non empty TopSpace; :: thesis: ( X is locally_connected implies for S being Subset of X st S is_a_component_of X holds
S is open )
assume A1: X is locally_connected ; :: thesis: for S being Subset of X st S is_a_component_of X holds
S is open
let S be Subset of X; :: thesis: ( S is_a_component_of X implies S is open )
assume A2: S is_a_component_of X ; :: thesis: S is open
A3: Int S c= S by TOPS_1:44;

now

let p be set ; :: thesis: ( p in S implies p in Int S )
assume A4: p in S ; :: thesis: p in Int S
then reconsider x = p as Point of X ;
A5: X is_locally_connected_in x by A1, Def4;
A6: S is_a_component_of [#] X by A2, Th13;
[#] X is a_neighborhood of x by Th5, TOPS_1:53;
then S is a_neighborhood of x by A4, A5, A6, Th19;
hence p in Int S by Def1; :: thesis: verum

end;

then S c= Int S by TARSKI:def 3;
then Int S = S by A3, XBOOLE_0:def 10;
hence S is open by TOPS_1:55; :: thesis: verum