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 & A = [(PDir X),2] & Y is being_line & X is being_plane 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 & A = [(PDir X),2] & Y is being_line & X is being_plane 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 & A = [(PDir X),2] & Y is being_line & X is being_plane holds
( a on A iff Y '||' X )
let A be LINE of (IncProjSp_of AS); :: thesis: ( a = LDir Y & A = [(PDir X),2] & Y is being_line & X is being_plane implies ( a on A iff Y '||' X ) )
assume A1: ( a = LDir Y & A = [(PDir X),2] & Y is being_line & X is being_plane ) ; :: 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: for K being Subset of AS holds
( not K is being_line or not [(PDir X),2] = [K,1] or ( not ( LDir Y in the carrier of AS & LDir Y in K ) & not LDir Y = LDir K ) ) by ZFMISC_1:33;

now

given K, X' being Subset of AS such that A5: ( K is being_line & X' is being_plane & LDir Y = LDir K & [(PDir X),2] = [(PDir X'),2] & K '||' X' ) ; :: thesis: Y '||' X
A6: ( K is being_line & X' is being_plane & LDir Y = LDir K & PDir X = PDir X' & K '||' X' ) by A5, ZFMISC_1:33;
A7: ( K in AfLines AS & X' in AfPlanes AS ) by A5;
A8: ( LDir Y = Class (LinesParallelity AS),Y & Class (LinesParallelity AS),K = LDir K ) by A1, A5, Def5;
then Y in Class (LinesParallelity AS),K by A5, A7, EQREL_1:31;
then consider K' being Subset of AS such that
A9: ( Y = K' & K' is being_line & K '||' K' ) by A5, A8, Th9;
A10: ( Class (PlanesParallelity AS),X = PDir X & Class (PlanesParallelity AS),X' = PDir X' ) by A1, A5, Def6;
then X in Class (PlanesParallelity AS),X' by A6, A7, EQREL_1:31;
then A11: ex X'' being Subset of AS st
( X = X'' & X'' is being_plane & X' '||' X'' ) by A5, A10, Th10;
K // K' by A5, A9, AFF_4:40;
then K' '||' X' by A5, AFF_4:56;
hence Y '||' X by A5, A9, A11, AFF_4:59, AFF_4:60; :: thesis: verum

end;

hence Y '||' X by A1, A3, A4, Def11; :: thesis: verum

end;

now

assume Y '||' X ; :: thesis: a on A
then [(LDir Y),[(PDir X),2]] in Proj_Inc AS by A1, Def11;
hence a on A by A1, INCSP_1:def 1; :: thesis: verum

end;

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