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
now :: thesis: for p being object st p in S holds
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;
then ( Int S c= S & S c= Int S ) by TOPS_1:16;
then Int S = S by XBOOLE_0:def 10;
hence S is open ; :: thesis: verum