let D be non empty set ; :: thesis:
let d0 be Element of D; :: thesis:
let Y be non empty TopSpace; :: thesis:
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 Subset of Y holds
( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) ) :: thesis:

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:
hence the carrier of Y = D ; :: thesis:

now

let A be Subset of Y; :: thesis:
reconsider B = A as Subset of (STS (D,d0)) by A1;
thus ( {d0} c= A implies A is closed ) :: thesis:

proof

assume {d0} c= A ; :: thesis:
then B is closed by Th24;
hence A is closed by A1, TOPS_3:79; :: thesis:

end;

thus ( not A is empty & A is closed implies {d0} c= A ) :: thesis:

proof

assume A2: not A is empty ; :: thesis:
assume A is closed ; :: thesis:
then B is closed by A1, TOPS_3:79;
hence {d0} c= A by A2, Th24; :: thesis:

end;

end;

hence 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 ) ) ; :: thesis:

end;

assume A3: the carrier of Y = D ; :: thesis:
assume A4: 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 ) ) ; :: thesis:

now

let A be Subset of Y; :: thesis:
let C be Subset of (STS (D,d0)); :: thesis:
assume A5: A = C ; :: thesis:

A6: now

assume A7: C is closed ; :: thesis:

now

per cases ;

case C = {} ; :: thesis:

hence A is closed by A5; :: thesis:

end;

case C <> {} ; :: thesis:

then {d0} c= A by A5, A7, Th24;
hence A is closed by A4; :: thesis:

end;

end;

end;

hence A is closed ; :: thesis:

end;

now

assume A8: A is closed ; :: thesis:

now

per cases ;

case A = {} ; :: thesis:

hence C is closed by A5; :: thesis:

end;

case A <> {} ; :: thesis:

then {d0} c= C by A4, A5, A8;
hence C is closed by Th24; :: thesis:

end;

end;

end;

hence C is closed ; :: thesis:

end;

hence ( A is closed iff C is closed ) by A6; :: thesis:

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 A3, TOPS_3:73; :: thesis: