let AS be AffinSpace; :: thesis: for Y, X being Subset of
for a being POINT of
for A being LINE of 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 ; :: thesis: for a being POINT of
for A being LINE of 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 ; :: thesis: for A being LINE of 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 ; :: 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

A6: now

given K, X' being Subset of such that A7: K is being_line and
A8: X' is being_plane and
A9: LDir Y = LDir K and
A10: [(PDir X),2] = [(PDir X'),2] and
A11: K '||' X' ; :: thesis: Y '||' X
A12: X' in AfPlanes AS by A8;
A13: Class (PlanesParallelity AS),X' = PDir X' ;
PDir X = PDir X' by A10, ZFMISC_1:33;
then X in Class (PlanesParallelity AS),X' by A12, EQREL_1:31;
then A14: ex X'' being Subset of st
( X = X'' & X'' is being_plane & X' '||' X'' ) by A8, A13, Th10;
K in AfLines AS by A7;
then A15: Y in Class (LinesParallelity AS),K by A9, EQREL_1:31;
Class (LinesParallelity AS),K = LDir K ;
then consider K' being Subset of such that
A16: Y = K' and
A17: K' is being_line and
A18: K '||' K' by A7, A15, Th9;
K // K' by A7, A17, A18, AFF_4:40;
then K' '||' X' 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 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;
hence Y '||' X by A1, A2, A19, A6, Def11; :: thesis: verum

end;

now

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