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 = [Y9,1] & Y9 is being_line holds
Y9 c= Y
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 = [Y9,1] & Y9 is being_line holds
Y9 c= Y
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 = [Y9,1] & Y9 is being_line holds
Y9 c= Y
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 = [Y9,1] & Y9 is being_line implies Y9 c= Y )
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 = [Y9,1]
and
A14:
Y9 is being_line
; Y9 c= Y
A15:
now ( b is Element of AS implies Y9 c= Y )assume
b is
Element of
AS
;
Y9 c= Ythen reconsider y =
b as
Element of
AS ;
A16:
now ( ex Xc being Subset of AS st
( c = LDir Xc & Xc is being_line ) implies Y9 c= Y )given Xc being
Subset of
AS such that A17:
c = LDir Xc
and A18:
Xc is
being_line
;
Y9 c= Y
Xc '||' X9
by A2, A7, A9, A17, A18, Th28;
then A19:
Xc // X9
by A2, A18, AFF_4:40;
Xc '||' Y9
by A11, A13, A14, A17, A18, Th28;
then
Xc // Y9
by A14, A18, AFF_4:40;
then A20:
X9 // Y9
by A19, AFF_1:44;
y in Y9
by A10, A13, Th26;
then A21:
Y9 = y * X9
by A2, A20, AFF_4:def 3;
y in X
by A6, A8, Th26;
hence
Y9 c= Y
by A2, A3, A4, A5, A21, AFF_4:28;
verum end; now ( c is Element of AS implies Y9 c= Y )assume
c is
Element of
AS
;
Y9 c= Ythen reconsider z =
c as
Element of
AS ;
A22:
z in Y9
by A11, A13, Th26;
y in Y9
by A10, A13, Th26;
then A23:
Y9 = Line (
y,
z)
by A12, A14, A22, AFF_1:57;
A24:
z in X9
by A7, A9, Th26;
y in X
by A6, A8, Th26;
hence
Y9 c= Y
by A3, A4, A5, A12, A24, A23, AFF_4:19;
verum end; hence
Y9 c= Y
by A16, Th20;
verum end;
now ( ex Xb being Subset of AS st
( b = LDir Xb & Xb is being_line ) implies Y9 c= Y )given Xb being
Subset of
AS such that A25:
b = LDir Xb
and A26:
Xb is
being_line
;
Y9 c= YA27:
now ( c is Element of AS implies Y9 c= Y )assume
c is
Element of
AS
;
Y9 c= Ythen reconsider y =
c as
Element of
AS ;
Xb '||' X
by A1, A6, A8, A25, A26, Th28;
then A28:
Xb // X
by A1, A26, AFF_4:40;
Xb '||' Y9
by A10, A13, A14, A25, A26, Th28;
then
Xb // Y9
by A14, A26, AFF_4:40;
then A29:
X // Y9
by A28, AFF_1:44;
y in Y9
by A11, A13, Th26;
then A30:
Y9 = y * X
by A1, A29, AFF_4:def 3;
y in X9
by A7, A9, Th26;
hence
Y9 c= Y
by A1, A3, A4, A5, A30, AFF_4:28;
verum end; now for Xc being Subset of AS holds
( not c = LDir Xc or not Xc is being_line )
Xb '||' Y9
by A10, A13, A14, A25, A26, Th28;
then A31:
Xb // Y9
by A14, A26, AFF_4:40;
given Xc being
Subset of
AS such that A32:
c = LDir Xc
and A33:
Xc is
being_line
;
contradiction
Xc '||' Y9
by A11, A13, A14, A32, A33, Th28;
then
Xc // Y9
by A14, A33, AFF_4:40;
then
Xc // Xb
by A31, AFF_1:44;
hence
contradiction
by A12, A25, A26, A32, A33, Th11;
verum end; hence
Y9 c= Y
by A27, Th20;
verum end;
hence
Y9 c= Y
by A15, Th20; verum