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} ) )
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} ) ) )
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;
case A in D ; :: thesis: A in D
hence A in D ; :: thesis: verum
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} )
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;
end;
end;
hence ( A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) ) ; :: thesis: verum