let V be RealLinearSpace; :: thesis: for P, Q, R being Element of V st P,Q,R are_collinear & P <> R & Q <> R & P <> Q holds
ex r being non zero non unit Real st
( r = affine-ratio (P,Q,R) & affine-ratio (P,R,Q) = op1 r & affine-ratio (Q,P,R) = op1 (op2 (op1 r)) & affine-ratio (Q,R,P) = op2 (op1 r) & affine-ratio (R,P,Q) = op1 (op2 r) & affine-ratio (R,Q,P) = op2 r )
let P, Q, R be Element of V; :: thesis: ( P,Q,R are_collinear & P <> R & Q <> R & P <> Q implies ex r being non zero non unit Real st
( r = affine-ratio (P,Q,R) & affine-ratio (P,R,Q) = op1 r & affine-ratio (Q,P,R) = op1 (op2 (op1 r)) & affine-ratio (Q,R,P) = op2 (op1 r) & affine-ratio (R,P,Q) = op1 (op2 r) & affine-ratio (R,Q,P) = op2 r ) )
assume that
A1: P,Q,R are_collinear and
A2: P <> R and
A3: Q <> R and
A4: P <> Q ; :: thesis: ex r being non zero non unit Real st
( r = affine-ratio (P,Q,R) & affine-ratio (P,R,Q) = op1 r & affine-ratio (Q,P,R) = op1 (op2 (op1 r)) & affine-ratio (Q,R,P) = op2 (op1 r) & affine-ratio (R,P,Q) = op1 (op2 r) & affine-ratio (R,Q,P) = op2 r )
A5: ( affine-ratio (P,Q,R) <> 0 & affine-ratio (P,Q,R) <> 1 ) by A1, A2, A3, A4, Th06, Th07;
reconsider r = affine-ratio (P,Q,R) as Element of REAL by XREAL_0:def 1;
reconsider r9 = r as non zero non unit Real by A5, Def01;
take r9 ; :: thesis: ( r9 = affine-ratio (P,Q,R) & affine-ratio (P,R,Q) = op1 r9 & affine-ratio (Q,P,R) = op1 (op2 (op1 r9)) & affine-ratio (Q,R,P) = op2 (op1 r9) & affine-ratio (R,P,Q) = op1 (op2 r9) & affine-ratio (R,Q,P) = op2 r9 )
( affine-ratio (P,R,Q) = 1 / r & affine-ratio (Q,P,R) = r / (r - 1) & affine-ratio (Q,R,P) = (r - 1) / r & affine-ratio (R,P,Q) = 1 / (1 - r) & affine-ratio (R,Q,P) = 1 - r ) by A1, A2, A3, A4, Th09, Th10, Th11, Th12, Th13;
hence ( r9 = affine-ratio (P,Q,R) & affine-ratio (P,R,Q) = op1 r9 & affine-ratio (Q,P,R) = op1 (op2 (op1 r9)) & affine-ratio (Q,R,P) = op2 (op1 r9) & affine-ratio (R,P,Q) = op1 (op2 r9) & affine-ratio (R,Q,P) = op2 r9 ) by Th01; :: thesis: verum