let AS be AffinSpace; :: thesis: for a being Element of the Points of (ProjHorizon AS)
for a9 being Element of the Points of (IncProjSp_of AS)
for A being Element of the Lines of (ProjHorizon AS)
for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
let a be Element of the Points of (ProjHorizon AS); :: thesis: for a9 being Element of the Points of (IncProjSp_of AS)
for A being Element of the Lines of (ProjHorizon AS)
for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
let a9 be Element of the Points of (IncProjSp_of AS); :: thesis: for A being Element of the Lines of (ProjHorizon AS)
for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
let A be Element of the Lines of (ProjHorizon AS); :: thesis: for A9 being LINE of (IncProjSp_of AS) st a9 = a & A9 = [A,2] holds
( a on A iff a9 on A9 )
let A9 be LINE of (IncProjSp_of AS); :: thesis: ( a9 = a & A9 = [A,2] implies ( a on A iff a9 on A9 ) )
assume that
A1: a9 = a and
A2: A9 = [A,2] ; :: thesis: ( a on A iff a9 on A9 )
consider X being Subset of AS such that
A3: a = LDir X and
A4: X is being_line by Th14;
consider Y being Subset of AS such that
A5: A = PDir Y and
A6: Y is being_plane by Th15;

A7: now :: thesis: ( a9 on A9 implies a on A )

assume a9 on A9 ; :: thesis: a on A
then X '||' Y by A1, A2, A3, A4, A5, A6, Th29;
hence a on A by A3, A4, A5, A6, Th36; :: thesis: verum

end;

now :: thesis: ( a on A implies a9 on A9 )

assume a on A ; :: thesis: a9 on A9
then X '||' Y by A3, A4, A5, A6, Th36;
hence a9 on A9 by A1, A2, A3, A4, A5, A6, Th29; :: thesis: verum

end;

hence ( a on A iff a9 on A9 ) by A7; :: thesis: verum