TrivExt D is DECOMPOSITION-like

proof

A1: the carrier of (space D) = D by Def10;
let A be Subset of XX; :: according to BORSUK_1:def 15 :: thesis: ( A in TrivExt D implies A is compact )
assume A in TrivExt D ; :: thesis: A is compact
then consider W being Point of XX such that
A2: A = (proj (TrivExt D)) . W by Th32;
A3: A = (Proj (TrivExt D)) . W by A2;

now

per cases ( W in the carrier of X or not W in the carrier of X ) ;

suppose W in the carrier of X ; :: thesis: A is compact

then reconsider W' = W as Point of X ;
A4: A = (Proj D) . W' by A3, Th76;
then reconsider B = A as Subset of X by A1, TARSKI:def 3;
B is compact by A1, A4, Def15;
hence A is compact by COMPTS_1:28; :: thesis: verum

end;

suppose not W in the carrier of X ; :: thesis: A is compact

then A = {W} by A3, Th77;
hence A is compact ; :: thesis: verum

end;

end;

end;

hence A is compact ; :: thesis: verum

end;

hence TrivExt D is DECOMPOSITION of XX ; :: thesis: verum