reconsider P = [.0,1.] as Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def 13;
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