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