let AS be AffinSpace; 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; 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); 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); ( 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
; ( 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; verum