TrivExt D is DECOMPOSITION-like

proof

let A be Subset of XX; :: according to BORSUK_1:def 12 :: 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
A1: A = (proj (TrivExt D)) . W by EQREL_1:68;
A2: A = (Proj (TrivExt D)) . W by A1;
A3: the carrier of (space D) = D by Def7;

now :: thesis: A is compact

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 W9 = W as Point of X ;
A4: A = (Proj D) . W9 by A2, Th33;
then reconsider B = A as Subset of X by A3, TARSKI:def 3;
B is compact by A3, A4, Def12;
hence A is compact by COMPTS_1:19; :: thesis: verum

end;

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

then A = {W} by A2, Th34;
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