let OAS be OAffinSpace; :: thesis: for a, b, c, d being Element of OAS st a,b '||' c,d & a,c '||' b,d & not LIN a,b,c holds
ex x being Element of OAS st
( LIN x,a,d & LIN x,b,c )
let a, b, c, d be Element of OAS; :: thesis: ( a,b '||' c,d & a,c '||' b,d & not LIN a,b,c implies ex x being Element of OAS st
( LIN x,a,d & LIN x,b,c ) )
assume A1: ( a,b '||' c,d & a,c '||' b,d & not LIN a,b,c ) ; :: thesis: ex x being Element of OAS st
( LIN x,a,d & LIN x,b,c )
then ( a,b // c,d & a,c // b,d ) by Th21;
then consider x being Element of OAS such that
A2: ( Mid a,x,d & Mid b,x,c ) by A1, Th30;
( LIN a,x,d & LIN b,x,c ) by A2, DIRAF:34;
then ( LIN x,a,d & LIN x,b,c ) by DIRAF:36;
hence ex x being Element of OAS st
( LIN x,a,d & LIN x,b,c ) ; :: thesis: verum