reconsider D = TrivDecomp X as u.s.c._decomposition of X by Th39;
take D ; :: thesis: D is DECOMPOSITION-like
let A be Subset of X; :: according to BORSUK_1:def 12 :: thesis: ( A in D implies A is compact )
assume A in D ; :: thesis: A is compact
then ex x being Point of X st A = {x} by Th26;
hence A is compact ; :: thesis: verum