let SAS be Semi_Affine_Space; 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; 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
; ( o,a,p are_collinear & qtrap o,p )
now ( 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;
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;
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;
( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) )assume
o,
p,
b are_collinear
;
( o,c,d are_collinear & p,c // b,d )hence
(
o,
c,
d are_collinear &
p,
c // b,
d )
by A2;
verum end;
hence
( o,a,p are_collinear & qtrap o,p )
; verum