let SAS be Semi_Affine_Space; :: thesis: for o, p being Element of SAS st qtrap o,p holds
ex q being Element of SAS st
( not o,p,q are_collinear & qtrap o,q )
let o, p be Element of SAS; :: thesis: ( qtrap o,p implies ex q being Element of SAS st
( not o,p,q are_collinear & qtrap o,q ) )
A1: o,p // o,p by Th1;
assume A2: qtrap o,p ; :: thesis: ex q being Element of SAS st
( not o,p,q are_collinear & qtrap o,q )
then A3: o <> p by Th103;
consider r being Element of SAS such that
A4: not o,p,r are_collinear by A2, Th25, Th103;
consider q being Element of SAS such that
A5: o,r,q are_collinear and
A6: qtrap o,q by Th101;
take q ; :: thesis: ( not o,p,q are_collinear & qtrap o,q )
( o <> q & o,r // o,q ) by A5, A6, Th103;
hence ( not o,p,q are_collinear & qtrap o,q ) by A3, A4, A6, A1, Th23; :: thesis: verum