let AS be AffinSpace; :: thesis: for X, Y 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 X, Y 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 that
A1: a = LDir Y and
A2: A = [(PDir X),2] and
A3: Y is being_line and
A4: X is being_plane ; :: thesis: ( a on A iff Y '||' X )

A5: now :: thesis: ( a on A implies Y '||' X )

A6: now :: thesis: ( ex K, X9 being Subset of AS st
( K is being_line & X9 is being_plane & LDir Y = LDir K & [(PDir X),2] = [(PDir X9),2] & K '||' X9 ) implies Y '||' X )

given K, X9 being Subset of AS such that A7: K is being_line and
A8: X9 is being_plane and
A9: LDir Y = LDir K and
A10: [(PDir X),2] = [(PDir X9),2] and
A11: K '||' X9 ; :: thesis: Y '||' X
A12: X9 in AfPlanes AS by A8;
A13: Class ((PlanesParallelity AS),X9) = PDir X9 ;
PDir X = PDir X9 by A10, XTUPLE_0:1;
then X in Class ((PlanesParallelity AS),X9) by A12, EQREL_1:23;
then A14: ex X99 being Subset of AS st
( X = X99 & X99 is being_plane & X9 '||' X99 ) by A8, A13, Th10;
K in AfLines AS by A7;
then A15: Y in Class ((LinesParallelity AS),K) by A9, EQREL_1:23;
Class ((LinesParallelity AS),K) = LDir K ;
then consider K9 being Subset of AS such that
A16: Y = K9 and
A17: K9 is being_line and
A18: K '||' K9 by A7, A15, Th9;
K // K9 by A7, A17, A18, AFF_4:40;
then K9 '||' X9 by A11, AFF_4:56;
hence Y '||' X by A8, A16, A14, AFF_4:59, AFF_4:60; :: thesis: verum

end;

assume a on A ; :: thesis: Y '||' X
then A19: [a,A] in the Inc of (IncProjSp_of AS) by INCSP_1:def 1;
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 XTUPLE_0:1;
hence Y '||' X by A1, A2, A19, A6, Def11; :: thesis: verum

end;

now :: thesis: ( Y '||' X implies a on A )

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

end;

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