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 & x in the carrier of XX ) by EQREL_1:def 6;
then consider A being set such that
A1: ( x in A & 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 A1, 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, TARSKI:def 1; :: thesis: verum