let X be non empty TopSpace; :: thesis: for A being Subset of X st A in TrivDecomp X holds

ex x being Point of X st A = {x}

let A be Subset of X; :: thesis: ( A in TrivDecomp X implies ex x being Point of X st A = {x} )

assume A in TrivDecomp X ; :: thesis: ex x being Point of X st A = {x}

then consider x being object such that

A1: x in the carrier of X and

A2: A = Class ((id the carrier of X),x) by EQREL_1:def 3;

reconsider x = x as Point of X by A1;

take x ; :: thesis: A = {x}

thus A = {x} by A2, EQREL_1:25; :: thesis: verum

ex x being Point of X st A = {x}

let A be Subset of X; :: thesis: ( A in TrivDecomp X implies ex x being Point of X st A = {x} )

assume A in TrivDecomp X ; :: thesis: ex x being Point of X st A = {x}

then consider x being object such that

A1: x in the carrier of X and

A2: A = Class ((id the carrier of X),x) by EQREL_1:def 3;

reconsider x = x as Point of X by A1;

take x ; :: thesis: A = {x}

thus A = {x} by A2, EQREL_1:25; :: thesis: verum