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 A being Subset of XX holds

( not A in TrivExt D or A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

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

for A being Subset of XX holds

( not A in TrivExt D or A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

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

( not A in TrivExt D or A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

let A be Subset of XX; :: thesis: ( not A in TrivExt D or A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

assume A1: A in TrivExt D ; :: thesis: ( A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

( not x in [#] X & A = {x} ) ) ; :: thesis: verum

for D being non empty a_partition of the carrier of X

for A being Subset of XX holds

( not A in TrivExt D or A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

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

for A being Subset of XX holds

( not A in TrivExt D or A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

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

( not A in TrivExt D or A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

let A be Subset of XX; :: thesis: ( not A in TrivExt D or A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

assume A1: A in TrivExt D ; :: thesis: ( A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) )

now :: thesis: ( ( A in D & A in D ) or ( A in { {p} where p is Point of XX : not p in the carrier of X } & ex x being Point of XX st

( not x in [#] X & A = {x} ) ) )end;

hence
( A in D or ex x being Point of XX st ( not x in [#] X & A = {x} ) ) )

per cases
( A in D or A in { {p} where p is Point of XX : not p in the carrier of X } )
by A1, XBOOLE_0:def 3;

end;

case
A in { {p} where p is Point of XX : not p in the carrier of X }
; :: thesis: ex x being Point of XX st

( not x in [#] X & A = {x} )

( not x in [#] X & A = {x} )

then consider x being Point of XX such that

A2: A = {x} and

A3: not x in the carrier of X ;

take x = x; :: thesis: ( not x in [#] X & A = {x} )

thus not x in [#] X by A3; :: thesis: A = {x}

thus A = {x} by A2; :: thesis: verum

end;A2: A = {x} and

A3: not x in the carrier of X ;

take x = x; :: thesis: ( not x in [#] X & A = {x} )

thus not x in [#] X by A3; :: thesis: A = {x}

thus A = {x} by A2; :: thesis: verum

( not x in [#] X & A = {x} ) ) ; :: thesis: verum