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

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