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 ) ) ) ) ) by TOPS_3:79, Th20; :: thesis:
assume A1: the carrier of Y = D ; :: thesis:
assume A2: 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 :: 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: C is closed ; :: thesis:

now :: thesis:

per cases ;

case C = {} ; :: thesis:

hence A is closed by A3; :: thesis:

end;

case C <> {} ; :: thesis:

then {d0} c= A by A3, A5, Th20;
hence A is closed by A2; :: thesis:

end;

end;

end;

hence A is closed ; :: thesis:

end;

now :: thesis:

assume A6: A is closed ; :: thesis:

now :: thesis:

per cases ;

case A = {} ; :: thesis:

hence C is closed by A3; :: thesis:

end;

case A <> {} ; :: thesis:

then {d0} c= C by A2, A3, A6;
hence C is closed by Th20; :: thesis:

end;

end;

end;

hence C is closed ; :: thesis:

end;

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