let AS be AffinSpace; :: thesis: for X, Y being Subset of AS
for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is being_line & Y is being_plane holds
( a on A iff X '||' Y )
let X, Y be Subset of AS; :: thesis: for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is being_line & Y is being_plane holds
( a on A iff X '||' Y )
let a be Element of the Points of (ProjHorizon AS); :: thesis: for A being Element of the Lines of (ProjHorizon AS) st a = LDir X & A = PDir Y & X is being_line & Y is being_plane holds
( a on A iff X '||' Y )
let A be Element of the Lines of (ProjHorizon AS); :: thesis: ( a = LDir X & A = PDir Y & X is being_line & Y is being_plane implies ( a on A iff X '||' Y ) )
assume that
A1: a = LDir X and
A2: A = PDir Y and
A3: X is being_line and
A4: Y is being_plane ; :: thesis: ( a on A iff X '||' Y )

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

assume a on A ; :: thesis: X '||' Y
then [a,A] in the Inc of (ProjHorizon AS) by INCSP_1:def 1;
then consider X9, Y9 being Subset of AS such that
A6: a = LDir X9 and
A7: A = PDir Y9 and
A8: X9 is being_line and
A9: Y9 is being_plane and
A10: X9 '||' Y9 by Def12;
X // X9 by A1, A3, A6, A8, Th11;
then A11: X '||' Y9 by A10, AFF_4:56;
Y9 '||' Y by A2, A4, A7, A9, Th13;
hence X '||' Y by A9, A11, AFF_4:59, AFF_4:60; :: thesis: verum

end;

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

assume X '||' Y ; :: thesis: a on A
then [a,A] in Inc_of_Dir AS by A1, A2, A3, A4, Def12;
hence a on A by INCSP_1:def 1; :: thesis: verum

end;

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