let X be non empty compact TopSpace; :: thesis: for F being Point of holds 0 <= ||.F.||
let F be Point of ; :: thesis: 0 <= ||.F.||
reconsider F1 = F as Point of by LMX01;
||.F.|| = ||.F1.|| by FUNCT_1:72;
hence 0 <= ||.F.|| by C0SP1:28; :: thesis: verum