let XX be non empty TopSpace; :: thesis: for X being non empty SubSpace of XX

for D being non empty a_partition of the carrier of X

for x being Point of XX st not x in the carrier of X holds

{x} in TrivExt D

let X be non empty SubSpace of XX; :: thesis: for D being non empty a_partition of the carrier of X

for x being Point of XX st not x in the carrier of X holds

{x} in TrivExt D

let D be non empty a_partition of the carrier of X; :: thesis: for x being Point of XX st not x in the carrier of X holds

{x} in TrivExt D

let x be Point of XX; :: thesis: ( not x in the carrier of X implies {x} in TrivExt D )

union (TrivExt D) = the carrier of XX by EQREL_1:def 4;

then consider A being set such that

A1: x in A and

A2: A in TrivExt D by TARSKI:def 4;

assume not x in the carrier of X ; :: thesis: {x} in TrivExt D

then not A in D by A1;

then A in { {p} where p is Point of XX : not p in the carrier of X } by A2, XBOOLE_0:def 3;

then ex p being Point of XX st

( A = {p} & not p in the carrier of X ) ;

hence {x} in TrivExt D by A1, A2, TARSKI:def 1; :: thesis: verum

for D being non empty a_partition of the carrier of X

for x being Point of XX st not x in the carrier of X holds

{x} in TrivExt D

let X be non empty SubSpace of XX; :: thesis: for D being non empty a_partition of the carrier of X

for x being Point of XX st not x in the carrier of X holds

{x} in TrivExt D

let D be non empty a_partition of the carrier of X; :: thesis: for x being Point of XX st not x in the carrier of X holds

{x} in TrivExt D

let x be Point of XX; :: thesis: ( not x in the carrier of X implies {x} in TrivExt D )

union (TrivExt D) = the carrier of XX by EQREL_1:def 4;

then consider A being set such that

A1: x in A and

A2: A in TrivExt D by TARSKI:def 4;

assume not x in the carrier of X ; :: thesis: {x} in TrivExt D

then not A in D by A1;

then A in { {p} where p is Point of XX : not p in the carrier of X } by A2, XBOOLE_0:def 3;

then ex p being Point of XX st

( A = {p} & not p in the carrier of X ) ;

hence {x} in TrivExt D by A1, A2, TARSKI:def 1; :: thesis: verum