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 & X is being_plane 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 & X is being_plane 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 & X is being_plane 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 & X is being_plane holds
not a on A
let A be LINE of (IncProjSp_of AS); :: thesis: ( x = a & [(PDir X),2] = A & X is being_plane implies not a on A )
assume A1: ( x = a & [(PDir X),2] = A & X is being_plane ) ; :: thesis: not a on A
assume a on A ; :: thesis: contradiction
then A2: [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def 1;

A3: now

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, MCART_1:7
.= 1 by MCART_1:7 ;
hence contradiction ; :: thesis: verum

end;

now

given K, X' being Subset of AS such that A5: ( K is being_line & X' is being_plane & x = LDir K & [(PDir X),2] = [(PDir X'),2] & K '||' X' ) ; :: thesis: contradiction
x in Dir_of_Lines AS by A5, 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;

hence contradiction by A1, A2, A3, Def11; :: thesis: verum