let AS be AffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( x = a & [(PDir X),2] = A implies not a on A )
assume that
A1: x = a and
A2: [(PDir X),2] = A ; :: thesis: not a on A

A3: now :: thesis: for K being Subset of AS holds
( not K is being_line or not [(PDir X),2] = [K,1] or ( not ( x in the carrier of AS & x in K ) & not x = LDir K ) )

given K being Subset of AS such that K is being_line and
A4: [(PDir X),2] = [K,1] and
( ( x in the carrier of AS & x in K ) or x = LDir K ) ; :: thesis: contradiction
2 = [K,1] `2 by A4
.= 1 ;
hence contradiction ; :: thesis: verum

end;

A5: now :: thesis: for K, X9 being Subset of AS holds
( not K is being_line or not X9 is being_plane or not x = LDir K or not [(PDir X),2] = [(PDir X9),2] or not K '||' X9 )

given K, X9 being Subset of AS such that A6: K is being_line and
X9 is being_plane and
A7: x = LDir K and
[(PDir X),2] = [(PDir X9),2] and
K '||' X9 ; :: thesis: contradiction
x in Dir_of_Lines AS by A6, A7, Th14;
then the carrier of AS /\ (Dir_of_Lines AS) <> {} by XBOOLE_0:def 4;
then the carrier of AS meets Dir_of_Lines AS by XBOOLE_0:def 7;
hence contradiction by Th16; :: thesis: verum

end;

assume a on A ; :: thesis: contradiction
then [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def 1;
hence contradiction by A1, A2, A3, A5, Def11; :: thesis: verum