:: deftheorem Def4 defines pr1 GEOMTRAP:def 4 :
for V being RealLinearSpace
for w, y, u being VECTOR of V st Gen w,y holds
for b₅ being Real holds
( b₅ = pr1 (w,y,u) iff ex b being Real st u = (b₅ * w) + (b * y) );