let AS be AffinSpace; for a, b being POINT of (IncProjSp_of AS)
for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let a, b be POINT of (IncProjSp_of AS); for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let A, K be LINE of (IncProjSp_of AS); ( a on A & a on K & b on A & b on K & not a = b implies A = K )
assume that
A1:
a on A
and
A2:
a on K
and
A3:
b on A
and
A4:
b on K
; ( a = b or A = K )
consider X being Subset of AS such that
A5:
( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) )
by Th23;
consider X9 being Subset of AS such that
A6:
( ( K = [X9,1] & X9 is being_line ) or ( K = [(PDir X9),2] & X9 is being_plane ) )
by Th23;
assume A7:
a <> b
; A = K
A8:
now ( ex Y being Subset of AS st
( a = LDir Y & Y is being_line ) implies A = K )given Y being
Subset of
AS such that A9:
a = LDir Y
and A10:
Y is
being_line
;
A = KA11:
now ( ex Y9 being Subset of AS st
( b = LDir Y9 & Y9 is being_line ) implies A = K )given Y9 being
Subset of
AS such that A12:
b = LDir Y9
and A13:
Y9 is
being_line
;
A = KA14:
not
Y // Y9
by A7, A9, A10, A12, A13, Th11;
A15:
for
Z being
Subset of
AS for
M being
LINE of
(IncProjSp_of AS) st
M = [Z,1] &
Z is
being_line &
a on M holds
not
b on M
proof
let Z be
Subset of
AS;
for M being LINE of (IncProjSp_of AS) st M = [Z,1] & Z is being_line & a on M holds
not b on Mlet M be
LINE of
(IncProjSp_of AS);
( M = [Z,1] & Z is being_line & a on M implies not b on M )
assume that A16:
M = [Z,1]
and A17:
Z is
being_line
;
( not a on M or not b on M )
assume A18:
(
a on M &
b on M )
;
contradiction
then
Y9 '||' Z
by A12, A13, A16, A17, Th28;
then A19:
Y9 // Z
by A13, A17, AFF_4:40;
Y '||' Z
by A9, A10, A16, A17, A18, Th28;
then
Y // Z
by A10, A17, AFF_4:40;
then
Y // Y9
by A19, AFF_1:44;
hence
contradiction
by A7, A9, A10, A12, A13, Th11;
verum
end; then A20:
Y9 '||' X
by A1, A3, A5, A12, A13, Th29;
A21:
Y9 '||' X9
by A2, A4, A6, A12, A13, A15, Th29;
A22:
Y '||' X9
by A2, A4, A6, A9, A10, A15, Th29;
Y '||' X
by A1, A3, A5, A9, A10, A15, Th29;
then
X '||' X9
by A1, A2, A3, A4, A5, A6, A10, A13, A15, A14, A22, A20, A21, Th5;
hence
A = K
by A1, A2, A3, A4, A5, A6, A15, Th13;
verum end; now ( b is Element of AS implies A = K )assume
b is
Element of
AS
;
A = Kthen reconsider y =
b as
Element of
AS ;
A23:
y in X9
by A4, A6, Th26, Th27;
A24:
y = b
;
then
Y '||' X9
by A2, A4, A6, A9, A10, Th27, Th28;
then A25:
Y // X9
by A4, A6, A10, A24, Th27, AFF_4:40;
Y '||' X
by A1, A3, A5, A9, A10, A24, Th27, Th28;
then
Y // X
by A3, A5, A10, A24, Th27, AFF_4:40;
then A26:
X // X9
by A25, AFF_1:44;
y in X
by A3, A5, Th26, Th27;
hence
A = K
by A3, A4, A5, A6, A23, A26, Th27, AFF_1:45;
verum end; hence
A = K
by A11, Th20;
verum end;
now ( a is Element of AS implies A = K )assume
a is
Element of
AS
;
A = Kthen reconsider x =
a as
Element of
AS ;
A27:
x = a
;
A28:
x in X9
by A2, A6, Th26, Th27;
A29:
x in X
by A1, A5, Th26, Th27;
A30:
now ( ex Y being Subset of AS st
( b = LDir Y & Y is being_line ) implies A = K )given Y being
Subset of
AS such that A31:
b = LDir Y
and A32:
Y is
being_line
;
A = K
Y '||' X9
by A2, A4, A6, A27, A31, A32, Th27, Th28;
then A33:
Y // X9
by A2, A6, A27, A32, Th27, AFF_4:40;
Y '||' X
by A1, A3, A5, A27, A31, A32, Th27, Th28;
then
Y // X
by A1, A5, A27, A32, Th27, AFF_4:40;
then
X // X9
by A33, AFF_1:44;
hence
A = K
by A1, A2, A5, A6, A29, A28, Th27, AFF_1:45;
verum end; now ( b is Element of AS implies A = K )assume
b is
Element of
AS
;
A = Kthen reconsider y =
b as
Element of
AS ;
A34:
y in X9
by A4, A6, Th26, Th27;
y in X
by A3, A5, Th26, Th27;
hence
A = K
by A1, A2, A7, A5, A6, A29, A28, A34, Th27, AFF_1:18;
verum end; hence
A = K
by A30, Th20;
verum end;
hence
A = K
by A8, Th20; verum