:: deftheorem Def03 defines cross-ratio-tuple ANPROJ10:def 30 :
for V being RealLinearSpace
for x being Tuple of 4, the carrier of V
for b₃ being Real holds
( b₃ = cross-ratio-tuple x iff ex P, Q, R, S being Element of V st
( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b₃ = cross-ratio (P,Q,R,S) ) );