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