reconsider P = [.0 ,1.] as Subset of (TopSpaceMetr RealSpace ) by Lm3, METRIC_1:def 14;
let I1, I2 be TopStruct ; :: thesis: ( ( for P being Subset of (TopSpaceMetr RealSpace ) st P = [.0 ,1.] holds
I1 = (TopSpaceMetr RealSpace ) | P ) & ( for P being Subset of (TopSpaceMetr RealSpace ) st P = [.0 ,1.] holds
I2 = (TopSpaceMetr RealSpace ) | P ) implies I1 = I2 )
assume that
A1: for P being Subset of (TopSpaceMetr RealSpace ) st P = [.0 ,1.] holds
I1 = (TopSpaceMetr RealSpace ) | P and
A2: for P being Subset of (TopSpaceMetr RealSpace ) st P = [.0 ,1.] holds
I2 = (TopSpaceMetr RealSpace ) | P ; :: thesis: I1 = I2
I1 = (TopSpaceMetr RealSpace ) | P by A1;
hence I1 = I2 by A2; :: thesis: verum