let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) holds |.|(p,q)|.| <= |.p.| * |.q.|
let p, q be Point of (TOP-REAL n); :: thesis: |.|(p,q)|.| <= |.p.| * |.q.|
( len p = n & len q = n ) by CARD_1:def 7;
hence |.|(p,q)|.| <= |.p.| * |.q.| by Th14; :: thesis: verum