let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for e being Point of (Euclid n) st e = p holds
{ (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } = { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum }
let p be Point of (TOP-REAL n); :: thesis: for e being Point of (Euclid n) st e = p holds
{ (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } = { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum }
let e be Point of (Euclid n); :: thesis: ( e = p implies { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } = { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum } )
assume A1: e = p ; :: thesis: { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } = { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum }
A2: for m being non zero Element of NAT holds OpenHypercube (e,(1 / m)) = OpenHypercube (p,(1 / m))
proof
let m be non zero Element of NAT ; :: thesis: OpenHypercube (e,(1 / m)) = OpenHypercube (p,(1 / m))
consider e0 being Point of (Euclid n) such that
A3: p = e0 and
A4: OpenHypercube (e0,(1 / m)) = OpenHypercube (p,(1 / m)) by TIETZE_2:def 1;
thus OpenHypercube (e,(1 / m)) = OpenHypercube (p,(1 / m)) by A1, A3, A4; :: thesis: verum
end;
set XE = { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } ;
set XTR = { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum } ;
thus { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } c= { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum } :: according to XBOOLE_0:def 10 :: thesis: { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum } c= { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } or x in { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum } )
assume x in { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } ; :: thesis: x in { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum }
then consider me being non zero Element of NAT such that
A6: x = OpenHypercube (e,(1 / me)) ;
x = OpenHypercube (p,(1 / me)) by A6, A2;
hence x in { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum } or x in { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } )
assume x in { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum } ; :: thesis: x in { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum }
then consider mtr being non zero Element of NAT such that
A7: x = OpenHypercube (p,(1 / mtr)) ;
x = OpenHypercube (e,(1 / mtr)) by A7, A2;
hence x in { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } ; :: thesis: verum