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} ) ) ) ) ) :: 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:
let A be Subset of Y; :: thesis:
reconsider B = A as Subset of (STS D,d0) by A1;
thus ( A c= D \ {d0} implies A is open ) :: thesis:

proof

assume A c= D \ {d0} ; :: thesis:
then B is open by Th26;
hence A is open by A1, TOPS_3:76; :: thesis:

end;

thus ( A <> D & A is open implies A c= D \ {d0} ) :: thesis:

proof

assume A2: A <> D ; :: thesis:
assume A is open ; :: thesis:
then B is open by A1, TOPS_3:76;
hence A c= D \ {d0} by A2, Th26; :: thesis:

end;

end;

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

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: A is open ; :: thesis:

now

per cases ;

case A = D ; :: thesis:

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

end;

case A <> D ; :: thesis:

then A c= D \ {d0} by A4, A7;
hence C is open by A5, Th26; :: thesis:

end;

end;

end;

hence C is open ; :: thesis:

end;

now

assume A8: C is open ; :: thesis:

now

per cases ;

case C = D ; :: thesis:

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

end;

case C <> D ; :: thesis:

then A c= D \ {d0} by A5, A8, Th26;
hence A is open by A4; :: thesis:

end;

end;

end;

hence A is open ; :: thesis:

end;

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