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 A1: ( ( 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 ) ) ; :: thesis: I1 = I2
reconsider P = [.0 ,1.] as Subset of (TopSpaceMetr RealSpace ) by Lm3, METRIC_1:def 14;
( I1 = (TopSpaceMetr RealSpace ) | P & I2 = (TopSpaceMetr RealSpace ) | P ) by A1;
hence I1 = I2 ; :: thesis: verum