let T1, T2 be non empty TopSpace; :: thesis: for B1 being Neighborhood_System of T1
for B2 being Neighborhood_System of T2 st B1 = B2 holds
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
let B1 be Neighborhood_System of T1; :: thesis: for B2 being Neighborhood_System of T2 st B1 = B2 holds
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
let B2 be Neighborhood_System of T2; :: thesis: ( B1 = B2 implies TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) )
A1: dom B1 = the carrier of T1 by PARTFUN1:def 2;
A2: dom B2 = the carrier of T2 by PARTFUN1:def 2;
A3: UniCl (Union B2) = the topology of T2 by YELLOW_9:22;
A4: UniCl (Union B1) = the topology of T1 by YELLOW_9:22;
assume B1 = B2 ; :: thesis: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
hence TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) by A4, A3, A1, A2; :: thesis: verum