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 that
A1: x = a and
A2: [X,1] = A ; :: thesis: ( a on A iff ( X is being_line & x in X ) )

A3: now :: thesis: ( a on A implies ( X is being_line & x in X ) )

A4: now :: thesis: ( ex K being Subset of AS st
( K is being_line & [X,1] = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) implies ( X is being_line & x in X ) )

given K being Subset of AS 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 :: thesis: not x = LDir K

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
.= K ;
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, X9 being Subset of AS holds
( not K is being_line or not X9 is being_plane or not x = LDir K or not [X,1] = [(PDir X9),2] or not K '||' X9 ) by XTUPLE_0:1;
hence ( X is being_line & x in X ) by A1, A2, A9, A4, Def11; :: thesis: verum

end;

now :: thesis: ( X is being_line & x in X implies a on A )

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