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

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