let OAS be OAffinSpace; :: thesis: for a, b, c, d being Element of OAS holds
( not a,b '||' c,d or a,c '||' b,d or ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x ) )
let a, b, c, d be Element of OAS; :: thesis: ( not a,b '||' c,d or a,c '||' b,d or ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x ) )
assume A1: a,b '||' c,d ; :: thesis: ( a,c '||' b,d or ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x ) )
assume A2: not a,c '||' b,d ; :: thesis: ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x )

A3: now

assume a = b ; :: thesis: ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x )
then ( LIN a,c,a & LIN b,d,a ) by DIRAF:37;
hence ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x ) ; :: thesis: verum

end;

now

assume A4: a <> b ; :: thesis: ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x )
consider z being Element of OAS such that
A5: ( a,b '||' c,z & a,c '||' b,z ) by DIRAF:31;

A6: now

assume b = z ; :: thesis: ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x )
then b,a '||' b,c by A5, DIRAF:27;
then LIN b,a,c by DIRAF:def 5;
then ( LIN a,c,b & LIN b,d,b ) by DIRAF:36, DIRAF:37;
hence ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x ) ; :: thesis: verum

end;

now

assume A7: b <> z ; :: thesis: ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x )
c,d '||' c,z by A1, A4, A5, DIRAF:28;
then LIN c,d,z by DIRAF:def 5;
then LIN d,c,z by DIRAF:36;
then d,c '||' d,z by DIRAF:def 5;
then z,d '||' d,c by DIRAF:27;
then consider t being Element of OAS such that
A8: ( b,d '||' d,t & b,z '||' c,t ) by A2, A5, DIRAF:32;
a,c '||' c,t by A5, A7, A8, DIRAF:28;
then ( c,a '||' c,t & d,b '||' d,t ) by A8, DIRAF:27;
then ( LIN c,a,t & LIN d,b,t ) by DIRAF:def 5;
then ( LIN a,c,t & LIN b,d,t ) by DIRAF:36;
hence ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x ) ; :: thesis: verum

end;

hence ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x ) by A6; :: thesis: verum

end;

hence ex x being Element of OAS st
( LIN a,c,x & LIN b,d,x ) by A3; :: thesis: verum