let AS be AffinSpace; :: thesis: for X, Y, X9, Y9 being Subset of AS
for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds
( Y9 '||' Y & Y '||' Y9 )
let X, Y, X9, Y9 be Subset of AS; :: thesis: for b, c being POINT of (IncProjSp_of AS)
for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds
( Y9 '||' Y & Y '||' Y9 )
let b, c be POINT of (IncProjSp_of AS); :: thesis: for A, K, M being LINE of (IncProjSp_of AS) st X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane holds
( Y9 '||' Y & Y '||' Y9 )
let A, K, M be LINE of (IncProjSp_of AS); :: thesis: ( X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X,1] & K = [X9,1] & b on A & c on K & b on M & c on M & b <> c & M = [(PDir Y9),2] & Y9 is being_plane implies ( Y9 '||' Y & Y '||' Y9 ) )
assume that
A1: X is being_line and
A2: X9 is being_line and
A3: Y is being_plane and
A4: X c= Y and
A5: X9 c= Y and
A6: A = [X,1] and
A7: K = [X9,1] and
A8: b on A and
A9: c on K and
A10: b on M and
A11: c on M and
A12: b <> c and
A13: M = [(PDir Y9),2] and
A14: Y9 is being_plane ; :: thesis: ( Y9 '||' Y & Y '||' Y9 )
( b is Element of AS or ex Xb being Subset of AS st
( b = LDir Xb & Xb is being_line ) ) by Th20;
then consider Xb being Subset of AS such that
A15: b = LDir Xb and
A16: Xb is being_line by A10, A13, Th27;
A17: Xb '||' Y9 by A10, A13, A14, A15, A16, Th29;
Xb '||' X by A1, A6, A8, A15, A16, Th28;
then Xb // X by A1, A16, AFF_4:40;
then A18: Xb '||' Y by A1, A3, A4, AFF_4:42, AFF_4:56;
( c is Element of AS or ex Xc being Subset of AS st
( c = LDir Xc & Xc is being_line ) ) by Th20;
then consider Xc being Subset of AS such that
A19: c = LDir Xc and
A20: Xc is being_line by A11, A13, Th27;
A21: Xc '||' Y9 by A11, A13, A14, A19, A20, Th29;
Xc '||' X9 by A2, A7, A9, A19, A20, Th28;
then Xc // X9 by A2, A20, AFF_4:40;
then A22: Xc '||' Y by A2, A3, A5, AFF_4:42, AFF_4:56;
not Xb // Xc by A12, A15, A16, A19, A20, Th11;
hence ( Y9 '||' Y & Y '||' Y9 ) by A3, A14, A16, A20, A17, A21, A18, A22, Th5; :: thesis: verum