let S1, S2 be FMT_TopSpace; :: thesis: ( the carrier of S1 = the carrier of T & Family_open_set S1 = the topology of T & the carrier of S2 = the carrier of T & Family_open_set S2 = the topology of T implies S1 = S2 )
assume that
A1: ( the carrier of S1 = the carrier of T & Family_open_set S1 = the topology of T ) and
A2: ( the carrier of S2 = the carrier of T & Family_open_set S2 = the topology of T ) ; :: thesis: S1 = S2
set F1 = the BNbd of S1;
set F2 = the BNbd of S2;
the BNbd of S1 = the BNbd of S2

proof

reconsider F2 = the BNbd of S2 as Function of the carrier of S1,(bool (bool the carrier of S1)) by A1, A2;
for x being object st x in the carrier of S1 holds
the BNbd of S1 . x = F2 . x

proof

let x be object ; :: thesis: ( x in the carrier of S1 implies the BNbd of S1 . x = F2 . x )
assume x in the carrier of S1 ; :: thesis: the BNbd of S1 . x = F2 . x
then reconsider x = x as Element of S1 ;
the BNbd of S1 . x = F2 . x

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: F2 . x c= the BNbd of S1 . x

let t be object ; :: thesis: ( t in the BNbd of S1 . x implies t in F2 . x )
assume t in the BNbd of S1 . x ; :: thesis: t in F2 . x
then t in U_FMT x ;
then t in { V where V is Subset of S1 : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } by A1, Th13;
then consider V1 being Subset of S1 such that
A3: t = V1 and
A4: ex O being Subset of T st
( O in the topology of T & x in O & O c= V1 ) ;
consider O1 being Subset of T such that
A5: ( O1 in the topology of T & x in O1 & O1 c= V1 ) by A4;
reconsider V2 = V1 as Subset of S2 by A1, A2;
reconsider x2 = x as Element of S2 by A1, A2;
( O1 in the topology of T & x2 in O1 & O1 c= V2 ) by A5;
then t in { V where V is Subset of S2 : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } by A3;
then t in U_FMT x2 by A2, Th13;
hence t in F2 . x ; :: thesis: verum

end;

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in F2 . x or t in the BNbd of S1 . x )
assume A6: t in F2 . x ; :: thesis: t in the BNbd of S1 . x
consider x3 being Element of S2 such that
A7: x = x3 by A1, A2;
t in U_FMT x3 by A7, A6;
then t in { V where V is Subset of S2 : ex O being Subset of T st
( O in the topology of T & x3 in O & O c= V ) } by A2, Th13;
then consider V2 being Subset of S2 such that
A8: t = V2 and
A9: ex O being Subset of T st
( O in the topology of T & x3 in O & O c= V2 ) ;
consider O2 being Subset of T such that
A10: ( O2 in the topology of T & x3 in O2 & O2 c= V2 ) by A9;
reconsider V1 = V2 as Subset of S1 by A1, A2;
reconsider x1 = x3 as Element of S1 by A1, A2;
( O2 in the topology of T & x1 in O2 & O2 c= V1 ) by A10;
then t in { V where V is Subset of S1 : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } by A7, A8;
then t in U_FMT x1 by A7, A1, Th13;
hence t in the BNbd of S1 . x by A7; :: thesis: verum

end;

hence the BNbd of S1 . x = F2 . x ; :: thesis: verum

end;

hence the BNbd of S1 = the BNbd of S2 by FUNCT_2:12; :: thesis: verum

end;

hence S1 = S2 ; :: thesis: verum