dom x = Seg 4 by FINSEQ_2:124;
then ( 1 in dom x & 2 in dom x & 3 in dom x & 4 in dom x ) ;
then reconsider P = x . 1, Q = x . 2, R = x . 3, S = x . 4 as Element of V by FINSEQ_2:11;
cross-ratio (P,Q,R,S) is Real ;
hence ex b₁ being Real 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) ) ; :: thesis: verum