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 & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
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 & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
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 & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let a be POINT of (IncProjSp_of AS); :: thesis: for A being LINE of (IncProjSp_of AS) st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let A be LINE of (IncProjSp_of AS); :: thesis: ( x = a & [X,1] = A implies ( a on A iff ( X is being_line & x in X ) ) )
assume A1: ( x = a & [X,1] = A ) ; :: thesis: ( a on A iff ( X is being_line & x in X ) )

A2: now

assume a on A ; :: thesis: ( X is being_line & x in X )
then A3: [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def 1;

A4: now

given K being Subset of AS such that A5: ( K is being_line & [X,1] = [K,1] ) and
A6: ( ( x in the carrier of AS & x in K ) or x = LDir K ) ; :: thesis: ( X is being_line & x in X )
A7: X = [K,1] `1 by A5, MCART_1:7
.= K by MCART_1:7 ;

now

assume x = LDir K ; :: thesis: contradiction
then 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 ( X is being_line & x in X ) by A5, A6, A7; :: thesis: verum

end;

for K, X' being Subset of AS holds
( not K is being_line or not X' is being_plane or not x = LDir K or not [X,1] = [(PDir X'),2] or not K '||' X' ) by ZFMISC_1:33;
hence ( X is being_line & x in X ) by A1, A3, A4, Def11; :: thesis: verum

end;

now

assume ( X is being_line & x in X ) ; :: thesis: a on A
then [x,[X,1]] in Proj_Inc AS by Def11;
hence a on A by A1, INCSP_1:def 1; :: thesis: verum

end;

hence ( a on A iff ( X is being_line & x in X ) ) by A2; :: thesis: verum