let AS be AffinSpace; :: thesis: for Y, X being Subset of AS
for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st a = LDir Y & [X,1] = A & Y is being_line & X is being_line holds
( a on A iff Y '||' X )
let Y, X be Subset of AS; :: thesis: for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) st a = LDir Y & [X,1] = A & Y is being_line & X is being_line holds
( a on A iff Y '||' X )
let a be POINT of (IncProjSp_of AS); :: thesis: for A being LINE of (IncProjSp_of AS) st a = LDir Y & [X,1] = A & Y is being_line & X is being_line holds
( a on A iff Y '||' X )
let A be LINE of (IncProjSp_of AS); :: thesis: ( a = LDir Y & [X,1] = A & Y is being_line & X is being_line implies ( a on A iff Y '||' X ) )
assume A1: ( a = LDir Y & [X,1] = A & Y is being_line & X is being_line ) ; :: thesis: ( a on A iff Y '||' X )

A2: now

assume a on A ; :: thesis: Y '||' 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: ( ( LDir Y in the carrier of AS & LDir Y in K ) or LDir Y = LDir K ) ; :: thesis: Y '||' X
A7: ( K is being_line & X = K ) by A5, ZFMISC_1:33;
A8: K in AfLines AS by A5;

A9: now

assume A10: ( LDir Y in the carrier of AS & LDir Y in K ) ; :: thesis: contradiction
a in Dir_of_Lines AS by A1, Th14;
then the carrier of AS /\ (Dir_of_Lines AS) <> {} by A1, A10, 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;

now

assume A11: LDir Y = LDir K ; :: thesis: Y '||' X
A12: ( LDir Y = Class (LinesParallelity AS),Y & LDir K = Class (LinesParallelity AS),K ) by A1, A5, Def5;
then Y in Class (LinesParallelity AS),K by A8, A11, EQREL_1:31;
then consider K' being Subset of AS such that
A13: ( Y = K' & K' is being_line & K '||' K' ) by A5, A12, Th9;
K // K' by A5, A13, AFF_4:40;
hence Y '||' X by A7, A13, AFF_4:40; :: thesis: verum

end;

hence Y '||' X by A6, A9; :: thesis: verum

end;

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

end;

now

assume Y '||' X ; :: thesis: a on A
then X in LDir Y by A1, Th9;
then ( X in Class (LinesParallelity AS),Y & Y in AfLines AS ) by A1, Def5;
then A14: Class (LinesParallelity AS),X = Class (LinesParallelity AS),Y by EQREL_1:31;
( LDir X = Class (LinesParallelity AS),X & LDir Y = Class (LinesParallelity AS),Y ) by A1, Def5;
then [a,A] in Proj_Inc AS by A1, A14, Def11;
hence a on A by INCSP_1:def 1; :: thesis: verum

end;

hence ( a on A iff Y '||' X ) by A2; :: thesis: verum