scheme :: JGRAPH_2:sch 3
ClosedSubset{ F1( Point of (TOP-REAL 2)) -> Real, F2( Point of (TOP-REAL 2)) -> Real } :
{ p where p is Point of (TOP-REAL 2) : F1(p) <= F2(p) } is closed Subset of (TOP-REAL 2)
provided
A1: for p, q being Point of (TOP-REAL 2) holds
( F1((p - q)) = F1(p) - F1(q) & F2((p - q)) = F2(p) - F2(q) ) and
A2: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (F1((p - q)) ^2) + (F2((p - q)) ^2)