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

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

hence
S1 = S2
; :: thesis: verum
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

end;for x being object st x in the carrier of S1 holds

the BNbd of S1 . x = F2 . x

proof

hence
the BNbd of S1 = the BNbd of S2
by FUNCT_2:12; :: thesis: verum
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

end;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

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: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: F2 . x c= the BNbd of S1 . x

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in F2 . x or t in 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;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

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