TrivExt D is DECOMPOSITION-like

proof

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

end;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 end;

hence
A is compact
; :: thesis: verumper cases
( W in the carrier of X or not W in the carrier of X )
;

end;