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 b1 being Real ex P, Q, R, S being Element of V st
( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b1 = cross-ratio (P,Q,R,S) )
; verum