let OAS be OAffinSpace; :: thesis: for a, b, c, p being Element of OAS st not p,a,b are_collinear & p,a '||' b,c & p,b '||' a,c holds
( p,a // b,c & p,b // a,c )
let a, b, c, p be Element of OAS; :: thesis: ( not p,a,b are_collinear & p,a '||' b,c & p,b '||' a,c implies ( p,a // b,c & p,b // a,c ) )
assume that
A1: not p,a,b are_collinear and
A2: p,a '||' b,c and
A3: p,b '||' a,c ; :: thesis: ( p,a // b,c & p,b // a,c )
consider d being Element of OAS such that
A4: p,a // b,d and
A5: p,b // a,d and
a <> d by ANALOAF:def 5;
A6: p,b '||' a,d by A5, DIRAF:def 4;
p,a '||' b,d by A4, DIRAF:def 4;
hence ( p,a // b,c & p,b // a,c ) by A1, A2, A3, A4, A5, A6, Th5; :: thesis: verum