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 is_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 is_collinear & qtrap o,q ) )
A1: o,p // o,p by Th12;
assume A2: qtrap o,p ; :: thesis: ex q being Element of SAS st
( not o,p,q is_collinear & qtrap o,q )
then A3: o <> p by Th131;
consider r being Element of SAS such that
A4: not o,p,r is_collinear by A2, Th41, Th131;
consider q being Element of SAS such that
A5: o,r,q is_collinear and
A6: qtrap o,q by Th129;
take q ; :: thesis: ( not o,p,q is_collinear & qtrap o,q )
( o <> q & o,r // o,q ) by A5, A6, Def2, Th131;
hence ( not o,p,q is_collinear & qtrap o,q ) by A3, A4, A6, A1, Th39; :: thesis: verum