let AS be AffinSpace; for x being Element of AS
for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
let x be Element of AS; for X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
let X be Subset of AS; for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
let a be POINT of (IncProjSp_of AS); for A being LINE of (IncProjSp_of AS) st x = a & [(PDir X),2] = A holds
not a on A
let A be LINE of (IncProjSp_of AS); ( x = a & [(PDir X),2] = A implies not a on A )
assume that
A1:
x = a
and
A2:
[(PDir X),2] = A
; not a on A
assume
a on A
; contradiction
then
[a,A] in the Inc of (IncProjSp_of AS)
by INCSP_1:def 1;
hence
contradiction
by A1, A2, A3, A5, Def11; verum