let SAS be Semi_Affine_Space; :: thesis: for o, p, c, b being Element of SAS st not o,p,c is_collinear & o,p,b is_collinear & qtrap o,p holds
ex d being Element of SAS st trap p,b,c,d,o
let o, p, c, b be Element of SAS; :: thesis: ( not o,p,c is_collinear & o,p,b is_collinear & qtrap o,p implies ex d being Element of SAS st trap p,b,c,d,o )
assume that
A1: ( not o,p,c is_collinear & o,p,b is_collinear ) and
A2: qtrap o,p ; :: thesis: ex d being Element of SAS st trap p,b,c,d,o
consider d being Element of SAS such that
A3: ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ) by A2, Def9;
take d ; :: thesis: trap p,b,c,d,o
thus trap p,b,c,d,o by A1, A3, Def8; :: thesis: verum