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