let SAS be Semi_Affine_Space; :: thesis: for o, a being Element of SAS ex p being Element of SAS st
( o,a,p is_collinear & qtrap o,p )
let o, a be Element of SAS; :: thesis: ex p being Element of SAS st
( o,a,p is_collinear & qtrap o,p )
consider p being Element of SAS such that
A1: for b, c being Element of SAS holds
( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) ) by Def1;
take p ; :: thesis: ( o,a,p is_collinear & qtrap o,p )

now

thus o,a,p is_collinear by A1, Def2; :: thesis: for b, c being Element of SAS ex d being Element of SAS st
( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) )
let b, c be Element of SAS; :: thesis: ex d being Element of SAS st
( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) )
consider d being Element of SAS such that
A2: ( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) by A1;
take d = d; :: thesis: ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) )
assume o,p,b is_collinear ; :: thesis: ( o,c,d is_collinear & p,c // b,d )
hence ( o,c,d is_collinear & p,c // b,d ) by A2, Def2; :: thesis: verum

end;

hence ( o,a,p is_collinear & qtrap o,p ) by Def9; :: thesis: verum