let SAS be Semi_Affine_Space; :: thesis: for o, a being Element of SAS ex p being Element of SAS st
( o,a,p are_collinear & qtrap o,p )
let o, a be Element of SAS; :: thesis: ex p being Element of SAS st
( o,a,p are_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 are_collinear & qtrap o,p )
now :: thesis: ( o,a,p are_collinear & ( for b, c being Element of SAS ex d being Element of SAS st
( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) ) ) )
thus o,a,p are_collinear by A1; :: thesis: for b, c being Element of SAS ex d being Element of SAS st
( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) )
let b, c be Element of SAS; :: thesis: ex d being Element of SAS st
( o,p,b are_collinear implies ( o,c,d are_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 are_collinear implies ( o,c,d are_collinear & p,c // b,d ) )
assume o,p,b are_collinear ; :: thesis: ( o,c,d are_collinear & p,c // b,d )
hence ( o,c,d are_collinear & p,c // b,d ) by A2; :: thesis: verum
end;
hence ( o,a,p are_collinear & qtrap o,p ) ; :: thesis: verum