let D be non empty set ; :: thesis: for d0 being Element of D
for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) )
let d0 be Element of D; :: thesis: for Y being non empty TopSpace holds
( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) )
let Y be non empty TopSpace; :: thesis: ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) )
thus ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) implies ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) ) :: thesis: ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) implies TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) )
proof
assume A1: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ; :: thesis: ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) )
hence the carrier of Y = D ; :: thesis: for A being non empty Subset of Y holds Cl A = A \/ {d0}
reconsider P = {d0} as Subset of Y by A1;
now :: thesis: for A being non empty Subset of Y holds Cl A = A \/ {d0}
let A be non empty Subset of Y; :: thesis: Cl A = A \/ {d0}
reconsider B = A as Subset of Y ;
not Cl A is empty by PCOMPS_1:2;
then A2: {d0} c= Cl A by A1, Th24;
A c= Cl A by PRE_TOPC:18;
then A3: A \/ {d0} c= Cl A by A2, XBOOLE_1:8;
{d0} c= A \/ P by XBOOLE_1:7;
then B \/ P is closed by A1, Th24;
then A4: Cl (A \/ P) = A \/ {d0} by PRE_TOPC:22;
Cl A c= Cl (A \/ P) by PRE_TOPC:19, XBOOLE_1:7;
hence Cl A = A \/ {d0} by A4, A3, XBOOLE_0:def 10; :: thesis: verum
end;
hence for A being non empty Subset of Y holds Cl A = A \/ {d0} ; :: thesis: verum
end;
assume A5: the carrier of Y = D ; :: thesis: ( ex A being non empty Subset of Y st not Cl A = A \/ {d0} or TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) )
assume A6: for A being non empty Subset of Y holds Cl A = A \/ {d0} ; :: thesis: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #)
now :: thesis: for A being Subset of Y holds
( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) )
let A be Subset of Y; :: thesis: ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) )
thus ( {d0} c= A implies A is closed ) :: thesis: ( not A is empty & A is closed implies {d0} c= A )
proof
assume {d0} c= A ; :: thesis: A is closed
then A = A \/ {d0} by XBOOLE_1:12;
then Cl A = A by A6;
hence A is closed ; :: thesis: verum
end;
thus ( not A is empty & A is closed implies {d0} c= A ) :: thesis: verum
proof
assume not A is empty ; :: thesis: ( not A is closed or {d0} c= A )
then A7: Cl A = A \/ {d0} by A6;
assume A is closed ; :: thesis: {d0} c= A
then A8: Cl A = A by PRE_TOPC:22;
assume not {d0} c= A ; :: thesis: contradiction
hence contradiction by A7, A8, XBOOLE_1:7; :: thesis: verum
end;
end;
hence TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) by A5, Th24; :: thesis: verum