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;
end;
end;
hence A is compact ; :: thesis: verum
end;
hence TrivExt D is DECOMPOSITION of XX ; :: thesis: verum