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

A4: now

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

end;

now

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

end;

hence ( a on A iff a' on A' ) by A4; :: thesis: verum