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
( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) ) by Th22, TOPS_3:76; :: thesis:
assume A1: the carrier of Y = D ; :: thesis:
assume A2: for A being Subset of Y holds
( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ; :: thesis:

now :: thesis:

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

A4: now :: thesis:

assume A5: A is open ; :: thesis:

now :: thesis:

per cases ;

case A = D ; :: thesis:

then C = [#] (STS (D,d0)) by A3;
hence C is open ; :: thesis:

end;

case A <> D ; :: thesis:

then A c= D \ {d0} by A2, A5;
hence C is open by A3, Th22; :: thesis:

end;

end;

end;

hence C is open ; :: thesis:

end;

now :: thesis:

assume A6: C is open ; :: thesis:

now :: thesis:

per cases ;

case C = D ; :: thesis:

then A = [#] Y by A1, A3;
hence A is open ; :: thesis:

end;

case C <> D ; :: thesis:

then A c= D \ {d0} by A3, A6, Th22;
hence A is open by A2; :: thesis:

end;

end;

end;

hence A is open ; :: thesis:

end;

hence ( A is open iff C is open ) by A4; :: 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 A1, TOPS_3:72; :: thesis: