let OAS be OAffinSpace; :: thesis: for a, b, c, d being Element of OAS st a,b '||' c,d & a,c '||' b,d & not a,b,c are_collinear holds

ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear )

let a, b, c, d be Element of OAS; :: thesis: ( a,b '||' c,d & a,c '||' b,d & not a,b,c are_collinear implies ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear ) )

assume that

A1: a,b '||' c,d and

A2: a,c '||' b,d and

A3: not a,b,c are_collinear ; :: thesis: ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear )

a,b // c,d by A1, A2, A3, Th14;

then consider x being Element of OAS such that

A4: Mid a,x,d and

A5: Mid b,x,c by A3, Th23;

b,x,c are_collinear by A5, DIRAF:28;

then A6: x,b,c are_collinear by DIRAF:30;

a,x,d are_collinear by A4, DIRAF:28;

then x,a,d are_collinear by DIRAF:30;

hence ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear ) by A6; :: thesis: verum

ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear )

let a, b, c, d be Element of OAS; :: thesis: ( a,b '||' c,d & a,c '||' b,d & not a,b,c are_collinear implies ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear ) )

assume that

A1: a,b '||' c,d and

A2: a,c '||' b,d and

A3: not a,b,c are_collinear ; :: thesis: ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear )

a,b // c,d by A1, A2, A3, Th14;

then consider x being Element of OAS such that

A4: Mid a,x,d and

A5: Mid b,x,c by A3, Th23;

b,x,c are_collinear by A5, DIRAF:28;

then A6: x,b,c are_collinear by DIRAF:30;

a,x,d are_collinear by A4, DIRAF:28;

then x,a,d are_collinear by DIRAF:30;

hence ex x being Element of OAS st

( x,a,d are_collinear & x,b,c are_collinear ) by A6; :: thesis: verum