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
( a,c,x are_collinear & b,d,x are_collinear ) )
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
( a,c,x are_collinear & b,d,x are_collinear ) )
assume A1: a,b '||' c,d ; :: thesis: ( a,c '||' b,d or ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) )
assume A2: not a,c '||' b,d ; :: thesis: ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear )
A3: now :: thesis: ( a <> b implies ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) )
consider z being Element of OAS such that
A4: a,b '||' c,z and
A5: a,c '||' b,z by DIRAF:26;
assume A6: a <> b ; :: thesis: ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear )
A7: now :: thesis: ( b <> z implies ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) )
c,d '||' c,z by A1, A6, A4, DIRAF:23;
then c,d,z are_collinear by DIRAF:def 5;
then d,c,z are_collinear by DIRAF:30;
then d,c '||' d,z by DIRAF:def 5;
then z,d '||' d,c by DIRAF:22;
then consider t being Element of OAS such that
A8: b,d '||' d,t and
A9: b,z '||' c,t by A2, A5, DIRAF:27;
assume b <> z ; :: thesis: ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear )
then a,c '||' c,t by A5, A9, DIRAF:23;
then c,a '||' c,t by DIRAF:22;
then c,a,t are_collinear by DIRAF:def 5;
then A10: a,c,t are_collinear by DIRAF:30;
d,b '||' d,t by A8, DIRAF:22;
then d,b,t are_collinear by DIRAF:def 5;
then b,d,t are_collinear by DIRAF:30;
hence ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) by A10; :: thesis: verum
end;
now :: thesis: ( b = z implies ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) )
assume b = z ; :: thesis: ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear )
then b,a '||' b,c by A4, DIRAF:22;
then b,a,c are_collinear by DIRAF:def 5;
then A11: a,c,b are_collinear by DIRAF:30;
b,d,b are_collinear by DIRAF:31;
hence ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) by A11; :: thesis: verum
end;
hence ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) by A7; :: thesis: verum
end;
now :: thesis: ( a = b implies ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) )
assume a = b ; :: thesis: ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear )
then ( a,c,a are_collinear & b,d,a are_collinear ) by DIRAF:31;
hence ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) ; :: thesis: verum
end;
hence ex x being Element of OAS st
( a,c,x are_collinear & b,d,x are_collinear ) by A3; :: thesis: verum