let AS be AffinSpace; :: thesis: for x being Element of
for X being Subset of
for a being POINT of
for A being LINE of st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let x be Element of ; :: thesis: for X being Subset of
for a being POINT of
for A being LINE of st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let X be Subset of ; :: thesis: for a being POINT of
for A being LINE of st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let a be POINT of ; :: thesis: for A being LINE of st x = a & [X,1] = A holds
( a on A iff ( X is being_line & x in X ) )
let A be LINE of ; :: thesis: ( x = a & [X,1] = A implies ( a on A iff ( X is being_line & x in X ) ) )
assume that
A1: x = a and
A2: [X,1] = A ; :: thesis: ( a on A iff ( X is being_line & x in X ) )

A3: now

A4: now

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

A8: 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;

X = [K,1] `1 by A6, MCART_1:7
.= K by MCART_1:7 ;
hence ( X is being_line & x in X ) by A5, A7, A8; :: thesis: verum

end;

assume a on A ; :: thesis: ( X is being_line & x in X )
then A9: [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def 1;
for K, X' being Subset of 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, A2, A9, A4, Def11; :: thesis: verum

end;

now

assume that
A10: X is being_line and
A11: x in X ; :: thesis: a on A
[x,[X,1]] in Proj_Inc AS by A10, A11, Def11;
hence a on A by A1, A2, INCSP_1:def 1; :: thesis: verum

end;

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