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 that
A1: a,b '||' c,d and
A2: a,c '||' b,d and
A3: not LIN a,b,c ; :: thesis: ex x being Element of OAS st
( LIN x,a,d & LIN x,b,c )
a,b // c,d by A1, A2, A3, Th21;
then consider x being Element of OAS such that
A4: Mid a,x,d and
A5: Mid b,x,c by A3, Th30;
LIN b,x,c by A5, DIRAF:34;
then A6: LIN x,b,c by DIRAF:36;
LIN a,x,d by A4, DIRAF:34;
then LIN x,a,d by DIRAF:36;
hence ex x being Element of OAS st
( LIN x,a,d & LIN x,b,c ) by A6; :: thesis: verum