incsp_1.miz
begin
definition
struct
IncProjStr
(# the
Points,
Lines -> non
empty
set,
the
Inc ->
Relation of the Points, the Lines #)
attr strict
strict;
end
definition
struct (
IncProjStr)
IncStruct
(# the
Points,
Lines,
Planes -> non
empty
set,
the
Inc ->
Relation of the Points, the Lines,
the
Inc2 ->
Relation of the Points, the Planes,
the
Inc3 ->
Relation of the Lines, the Planes #)
attr strict
strict;
end
definition
let S be
IncProjStr;
mode
POINT of S is
Element of the
Points of S;
mode
LINE of S is
Element of the
Lines of S;
end
definition
let S be
IncStruct;
mode
PLANE of S is
Element of the
Planes of S;
end
reserve S for
IncStruct;
reserve A,B,C,D for
POINT of S;
reserve L for
LINE of S;
reserve P for
PLANE of S;
reserve F,G for
Subset of the
Points of S;
definition
let S be
IncProjStr;
let A be
POINT of S, L be
LINE of S;
::
INCSP_1:def1
pred A
on L means
[A, L]
in the
Inc of S;
end
definition
let S;
let A be
POINT of S, P be
PLANE of S;
::
INCSP_1:def2
pred A
on P means
[A, P]
in the
Inc2 of S;
end
definition
let S;
let L be
LINE of S, P be
PLANE of S;
::
INCSP_1:def3
pred L
on P means
[L, P]
in the
Inc3 of S;
end
definition
let S be
IncProjStr;
let F be
Subset of the
Points of S, L be
LINE of S;
::
INCSP_1:def4
pred F
on L means for A be
POINT of S st A
in F holds A
on L;
end
definition
let S;
let F be
Subset of the
Points of S, P be
PLANE of S;
::
INCSP_1:def5
pred F
on P means for A st A
in F holds A
on P;
end
definition
let S be
IncProjStr;
let F be
Subset of the
Points of S;
::
INCSP_1:def6
attr F is
linear means ex L be
LINE of S st F
on L;
end
definition
let S be
IncStruct;
let F be
Subset of the
Points of S;
::
INCSP_1:def7
attr F is
planar means ex P be
PLANE of S st F
on P;
end
theorem ::
INCSP_1:1
Th1: for S be
IncProjStr, L be
LINE of S, A,B be
POINT of S holds
{A, B}
on L iff A
on L & B
on L
proof
let S be
IncProjStr, L be
LINE of S, A,B be
POINT of S;
thus
{A, B}
on L implies A
on L & B
on L
proof
A1: A
in
{A, B} & B
in
{A, B} by
TARSKI:def 2;
assume
{A, B}
on L;
hence thesis by
A1;
end;
assume
A2: A
on L & B
on L;
let C be
POINT of S;
assume C
in
{A, B};
hence thesis by
A2,
TARSKI:def 2;
end;
theorem ::
INCSP_1:2
Th2: for S be
IncProjStr, L be
LINE of S, A,B,C be
POINT of S holds
{A, B, C}
on L iff A
on L & B
on L & C
on L
proof
let S be
IncProjStr, L be
LINE of S, A,B,C be
POINT of S;
thus
{A, B, C}
on L implies A
on L & B
on L & C
on L
proof
A1: C
in
{A, B, C} by
ENUMSET1:def 1;
A2: A
in
{A, B, C} & B
in
{A, B, C} by
ENUMSET1:def 1;
assume
{A, B, C}
on L;
hence thesis by
A2,
A1;
end;
assume
A3: A
on L & B
on L & C
on L;
let D be
POINT of S;
assume D
in
{A, B, C};
hence thesis by
A3,
ENUMSET1:def 1;
end;
theorem ::
INCSP_1:3
Th3:
{A, B}
on P iff A
on P & B
on P
proof
thus
{A, B}
on P implies A
on P & B
on P
proof
A1: A
in
{A, B} & B
in
{A, B} by
TARSKI:def 2;
assume
{A, B}
on P;
hence thesis by
A1;
end;
assume
A2: A
on P & B
on P;
let C be
POINT of S;
assume C
in
{A, B};
hence thesis by
A2,
TARSKI:def 2;
end;
theorem ::
INCSP_1:4
Th4:
{A, B, C}
on P iff A
on P & B
on P & C
on P
proof
thus
{A, B, C}
on P implies A
on P & B
on P & C
on P
proof
A1: C
in
{A, B, C} by
ENUMSET1:def 1;
A2: A
in
{A, B, C} & B
in
{A, B, C} by
ENUMSET1:def 1;
assume
{A, B, C}
on P;
hence thesis by
A2,
A1;
end;
assume
A3: A
on P & B
on P & C
on P;
let D be
POINT of S;
assume D
in
{A, B, C};
hence thesis by
A3,
ENUMSET1:def 1;
end;
theorem ::
INCSP_1:5
Th5:
{A, B, C, D}
on P iff A
on P & B
on P & C
on P & D
on P
proof
thus
{A, B, C, D}
on P implies A
on P & B
on P & C
on P & D
on P
proof
A1: C
in
{A, B, C, D} & D
in
{A, B, C, D} by
ENUMSET1:def 2;
A2: A
in
{A, B, C, D} & B
in
{A, B, C, D} by
ENUMSET1:def 2;
assume
{A, B, C, D}
on P;
hence thesis by
A2,
A1;
end;
assume
A3: A
on P & B
on P & C
on P & D
on P;
let E be
POINT of S;
assume E
in
{A, B, C, D};
hence thesis by
A3,
ENUMSET1:def 2;
end;
theorem ::
INCSP_1:6
Th6: G
c= F & F
on L implies G
on L;
theorem ::
INCSP_1:7
Th7: G
c= F & F
on P implies G
on P;
theorem ::
INCSP_1:8
Th8: F
on L & A
on L iff (F
\/
{A})
on L
proof
thus F
on L & A
on L implies (F
\/
{A})
on L
proof
assume
A1: F
on L & A
on L;
let C be
POINT of S;
assume C
in (F
\/
{A});
then C
in F or C
in
{A} by
XBOOLE_0:def 3;
hence thesis by
A1,
TARSKI:def 1;
end;
assume
A2: (F
\/
{A})
on L;
hence F
on L by
Th6,
XBOOLE_1: 7;
{A}
c= (F
\/
{A}) by
XBOOLE_1: 7;
then
{A, A}
c= (F
\/
{A}) by
ENUMSET1: 29;
then
{A, A}
on L by
A2;
hence thesis by
Th1;
end;
theorem ::
INCSP_1:9
Th9: F
on P & A
on P iff (F
\/
{A})
on P
proof
thus F
on P & A
on P implies (F
\/
{A})
on P
proof
assume
A1: F
on P & A
on P;
let C be
POINT of S;
assume C
in (F
\/
{A});
then C
in F or C
in
{A} by
XBOOLE_0:def 3;
hence thesis by
A1,
TARSKI:def 1;
end;
assume
A2: (F
\/
{A})
on P;
hence F
on P by
Th7,
XBOOLE_1: 7;
{A}
c= (F
\/
{A}) by
XBOOLE_1: 7;
then
{A, A}
c= (F
\/
{A}) by
ENUMSET1: 29;
then
{A, A}
on P by
A2;
hence thesis by
Th3;
end;
theorem ::
INCSP_1:10
Th10: (F
\/ G)
on L iff F
on L & G
on L
proof
thus (F
\/ G)
on L implies F
on L & G
on L by
Th6,
XBOOLE_1: 7;
assume
A1: F
on L & G
on L;
let C be
POINT of S;
assume C
in (F
\/ G);
then C
in F or C
in G by
XBOOLE_0:def 3;
hence thesis by
A1;
end;
theorem ::
INCSP_1:11
Th11: (F
\/ G)
on P iff F
on P & G
on P
proof
thus (F
\/ G)
on P implies F
on P & G
on P by
Th7,
XBOOLE_1: 7;
assume
A1: F
on P & G
on P;
let C be
POINT of S;
assume C
in (F
\/ G);
then C
in F or C
in G by
XBOOLE_0:def 3;
hence thesis by
A1;
end;
theorem ::
INCSP_1:12
G
c= F & F is
linear implies G is
linear
proof
assume that
A1: G
c= F and
A2: F is
linear;
consider L such that
A3: F
on L by
A2;
take L;
let A be
POINT of S;
assume A
in G;
hence thesis by
A1,
A3;
end;
theorem ::
INCSP_1:13
G
c= F & F is
planar implies G is
planar
proof
assume that
A1: G
c= F and
A2: F is
planar;
consider P such that
A3: F
on P by
A2;
take P;
let A be
POINT of S;
assume A
in G;
hence thesis by
A1,
A3;
end;
definition
let S be
IncProjStr;
::
INCSP_1:def8
attr S is
with_non-trivial_lines means
:
Def8: for L be
LINE of S holds ex A,B be
POINT of S st A
<> B &
{A, B}
on L;
::
INCSP_1:def9
attr S is
linear means
:
Def9: for A,B be
POINT of S holds ex L be
LINE of S st
{A, B}
on L;
::
INCSP_1:def10
attr S is
up-2-rank means
:
Def10: for A,B be
POINT of S, K,L be
LINE of S st A
<> B &
{A, B}
on K &
{A, B}
on L holds K
= L;
end
definition
let S be
IncStruct;
::
INCSP_1:def11
attr S is
with_non-empty_planes means
:
Def11: for P be
PLANE of S holds ex A be
POINT of S st A
on P;
::
INCSP_1:def12
attr S is
planar means
:
Def12: for A,B,C be
POINT of S holds ex P be
PLANE of S st
{A, B, C}
on P;
::
INCSP_1:def13
attr S is
with_<=1_plane_per_3_pts means
:
Def13: for A,B,C be
POINT of S, P,Q be
PLANE of S st not
{A, B, C} is
linear &
{A, B, C}
on P &
{A, B, C}
on Q holds P
= Q;
::
INCSP_1:def14
attr S is
with_lines_inside_planes means
:
Def14: for L be
LINE of S, P be
PLANE of S st ex A,B be
POINT of S st A
<> B &
{A, B}
on L &
{A, B}
on P holds L
on P;
::
INCSP_1:def15
attr S is
with_planes_intersecting_in_2_pts means
:
Def15: for A be
POINT of S, P,Q be
PLANE of S st A
on P & A
on Q holds ex B be
POINT of S st A
<> B & B
on P & B
on Q;
::
INCSP_1:def16
attr S is
up-3-dimensional means
:
Def16: ex A,B,C,D be
POINT of S st not
{A, B, C, D} is
planar;
::
INCSP_1:def17
attr S is
inc-compatible means
:
Def17: for A be
POINT of S, L be
LINE of S, P be
PLANE of S st A
on L & L
on P holds A
on P;
end
definition
let IT be
IncStruct;
::
INCSP_1:def18
attr IT is
IncSpace-like means IT is
with_non-trivial_lines
linear
up-2-rank
with_non-empty_planes
planar
with_<=1_plane_per_3_pts
with_lines_inside_planes
with_planes_intersecting_in_2_pts
up-3-dimensional
inc-compatible;
end
reserve a,b,c for
Element of
{
0 , 1, 2, 3};
registration
cluster
IncSpace-like ->
with_non-trivial_lines
linear
up-2-rank
with_non-empty_planes
planar
with_<=1_plane_per_3_pts
with_lines_inside_planes
with_planes_intersecting_in_2_pts
up-3-dimensional
inc-compatible for
IncStruct;
coherence ;
end
registration
cluster
strict
IncSpace-like for
IncStruct;
existence
proof
reconsider Zero1 =
0 , One = 1, Two = 2, Three = 3 as
Element of
{
0 , 1, 2, 3} by
ENUMSET1:def 2;
{Zero1, One}
in {
{a, b} where a be
Element of
{
0 , 1, 2, 3}, b be
Element of
{
0 , 1, 2, 3} : a
<> b };
then
reconsider Li = {
{a, b} where a be
Element of
{
0 , 1, 2, 3}, b be
Element of
{
0 , 1, 2, 3} : a
<> b } as non
empty
set;
{Zero1, One, Two}
in {
{a, b, c} where a be
Element of
{
0 , 1, 2, 3}, b be
Element of
{
0 , 1, 2, 3}, c be
Element of
{
0 , 1, 2, 3} : a
<> b & a
<> c & b
<> c };
then
reconsider Pl = {
{a, b, c} where a be
Element of
{
0 , 1, 2, 3}, b be
Element of
{
0 , 1, 2, 3}, c be
Element of
{
0 , 1, 2, 3} : a
<> b & a
<> c & b
<> c } as non
empty
set;
{
[a, l] where l be
Element of Li : a
in l }
c=
[:
{
0 , 1, 2, 3}, Li:]
proof
let x be
object;
assume x
in {
[a, l] where l be
Element of Li : a
in l };
then ex a be
Element of
{
0 , 1, 2, 3}, l be
Element of Li st x
=
[a, l] & a
in l;
hence thesis;
end;
then
reconsider i1 = {
[a, l] where l be
Element of Li : a
in l } as
Relation of
{
0 , 1, 2, 3}, Li;
{
[a, p] where p be
Element of Pl : a
in p }
c=
[:
{
0 , 1, 2, 3}, Pl:]
proof
let x be
object;
assume x
in {
[a, p] where p be
Element of Pl : a
in p };
then ex a st ex p be
Element of Pl st x
=
[a, p] & a
in p;
hence thesis;
end;
then
reconsider i2 = {
[a, p] where p be
Element of Pl : a
in p } as
Relation of
{
0 , 1, 2, 3}, Pl;
{
[l, p] where l be
Element of Li, p be
Element of Pl : l
c= p }
c=
[:Li, Pl:]
proof
let x be
object;
assume x
in {
[l, p] where l be
Element of Li, p be
Element of Pl : l
c= p };
then ex l be
Element of Li, p be
Element of Pl st x
=
[l, p] & l
c= p;
hence thesis;
end;
then
reconsider i3 = {
[l, p] where l be
Element of Li, p be
Element of Pl : l
c= p } as
Relation of Li, Pl;
now
set S =
IncStruct (#
{
0 , 1, 2, 3}, Li, Pl, i1, i2, i3 #);
thus S is
with_non-trivial_lines
proof
let L be
LINE of S;
reconsider l = L as
Element of Li;
l
in Li;
then
consider a, b such that
A1: l
=
{a, b} and
A2: a
<> b;
reconsider A = a, B = b as
POINT of S;
take A, B;
thus A
<> B by
A2;
b
in l by
A1,
TARSKI:def 2;
then
[b, l]
in i1;
then
A3: B
on L;
a
in l by
A1,
TARSKI:def 2;
then
[a, l]
in i1;
then A
on L;
hence thesis by
A3,
Th1;
end;
thus
A4: S is
linear
proof
let A,B be
POINT of S;
reconsider a = A, b = B as
Element of
{
0 , 1, 2, 3};
A5:
now
for a holds ex c st a
<> c
proof
let a;
A6:
now
assume a
= 1 or a
= 2 or a
= 3;
then a
<> Zero1;
hence thesis;
end;
now
assume a
=
0 ;
then a
<> One;
hence thesis;
end;
hence thesis by
A6,
ENUMSET1:def 2;
end;
then
consider c be
Element of
{
0 , 1, 2, 3} such that
A7: a
<> c;
{a, c}
in Li by
A7;
then
consider l be
Element of Li such that
A8: l
=
{a, c};
reconsider L = l as
LINE of S;
a
in l by
A8,
TARSKI:def 2;
then
[a, l]
in i1;
then
A9: A
on L;
assume a
= b;
then
{A, B}
on L by
A9,
Th1;
hence thesis;
end;
now
assume a
<> b;
then
{a, b}
in Li;
then
consider l be
Element of Li such that
A10: l
=
{a, b};
reconsider L = l as
LINE of S;
b
in l by
A10,
TARSKI:def 2;
then
[b, l]
in i1;
then
A11: B
on L;
a
in l by
A10,
TARSKI:def 2;
then
[a, l]
in i1;
then A
on L;
then
{A, B}
on L by
A11,
Th1;
hence thesis;
end;
hence thesis by
A5;
end;
A12: for l be
Element of Li holds
[a, l]
in i1 implies a
in l
proof
let l be
Element of Li;
assume
[a, l]
in i1;
then
consider b be
Element of
{
0 , 1, 2, 3}, k be
Element of Li such that
A13:
[a, l]
=
[b, k] and
A14: b
in k;
a
= b by
A13,
XTUPLE_0: 1;
hence thesis by
A13,
A14,
XTUPLE_0: 1;
end;
thus S is
up-2-rank
proof
let A,B be
POINT of S, K,L be
LINE of S;
assume that
A15: A
<> B and
A16:
{A, B}
on K and
A17:
{A, B}
on L;
reconsider a = A, b = B as
Element of
{
0 , 1, 2, 3};
reconsider k = K, l = L as
Element of Li;
k
in Li;
then
consider x1,x2 be
Element of
{
0 , 1, 2, 3} such that
A18: k
=
{x1, x2} and x1
<> x2;
B
on K by
A16,
Th1;
then
[b, k]
in i1;
then b
in k by
A12;
then
A19: b
= x1 or b
= x2 by
A18,
TARSKI:def 2;
l
in Li;
then
consider x3,x4 be
Element of
{
0 , 1, 2, 3} such that
A20: l
=
{x3, x4} and x3
<> x4;
A
on L by
A17,
Th1;
then
[a, l]
in i1;
then a
in l by
A12;
then
A21: a
= x3 or a
= x4 by
A20,
TARSKI:def 2;
B
on L by
A17,
Th1;
then
[b, l]
in i1;
then
A22: b
in l by
A12;
A
on K by
A16,
Th1;
then
[a, k]
in i1;
then a
in k by
A12;
then a
= x1 or a
= x2 by
A18,
TARSKI:def 2;
hence thesis by
A15,
A22,
A18,
A19,
A20,
A21,
TARSKI:def 2;
end;
thus S is
with_non-empty_planes
proof
let P be
PLANE of S;
reconsider p = P as
Element of Pl;
p
in Pl;
then
consider a, b, c such that
A23: p
=
{a, b, c} and a
<> b and a
<> c and b
<> c;
reconsider A = a as
POINT of S;
take A;
a
in p by
A23,
ENUMSET1:def 1;
then
[a, p]
in i2;
hence thesis;
end;
thus S is
planar
proof
let A,B,C be
POINT of S;
reconsider a = A, b = B, c = C as
Element of
{
0 , 1, 2, 3};
A24:
now
for a holds ex b, c st a
<> b & a
<> c & b
<> c
proof
let a;
A25:
now
assume a
= 2 or a
= 3;
then a
<> Zero1 & a
<> One;
hence thesis;
end;
now
assume a
=
0 or a
= 1;
then a
<> Two & a
<> Three;
hence thesis;
end;
hence thesis by
A25,
ENUMSET1:def 2;
end;
then
consider x,y be
Element of
{
0 , 1, 2, 3} such that
A26: a
<> x & a
<> y & x
<> y;
{a, x, y}
in Pl by
A26;
then
consider p be
Element of Pl such that
A27: p
=
{a, x, y};
reconsider P = p as
PLANE of S;
assume that
A28: a
= b & a
= c and b
= c;
a
in p by
A27,
ENUMSET1:def 1;
then
[a, p]
in i2;
then A
on P;
then
{A, B, C}
on P by
A28,
Th4;
hence thesis;
end;
A29:
now
assume
A30: a
= b & a
<> c or a
= c & a
<> b or b
= c & a
<> b;
then
consider x,y be
Element of
{
0 , 1, 2, 3} such that
A31: (x
= a or x
= b or x
= c) & (y
= a or y
= b or y
= c) and
A32: x
<> y;
for a, b holds ex c st a
<> c & b
<> c
proof
let a, b;
A33:
now
assume that
A34: a
=
0 and
A35: b
= 3;
a
<> One by
A34;
hence thesis by
A35;
end;
A36:
now
assume that
A37: a
= 1 or a
= 2 or a
= 3 and
A38: b
= 1 or b
= 2 or b
= 3;
a
<> Zero1 by
A37;
hence thesis by
A38;
end;
A39:
now
assume that
A40: a
= 3 and
A41: b
=
0 ;
a
<> Two by
A40;
hence thesis by
A41;
end;
A42:
now
assume that
A43: a
= 1 or a
= 2 and
A44: b
=
0 ;
a
<> Three by
A43;
hence thesis by
A44;
end;
now
assume that
A45: a
=
0 and
A46: b
=
0 or b
= 1 or b
= 2;
a
<> Three by
A45;
hence thesis by
A46;
end;
hence thesis by
A33,
A36,
A42,
A39,
ENUMSET1:def 2;
end;
then
consider z be
Element of
{
0 , 1, 2, 3} such that
A47: x
<> z & y
<> z;
{x, y, z}
in Pl by
A32,
A47;
then
consider p be
Element of Pl such that
A48: p
=
{x, y, z};
reconsider P = p as
PLANE of S;
b
in p by
A30,
A31,
A32,
A48,
ENUMSET1:def 1;
then
[b, p]
in i2;
then
A49: B
on P;
c
in p by
A30,
A31,
A32,
A48,
ENUMSET1:def 1;
then
[c, p]
in i2;
then
A50: C
on P;
a
in p by
A30,
A31,
A32,
A48,
ENUMSET1:def 1;
then
[a, p]
in i2;
then A
on P;
then
{A, B, C}
on P by
A49,
A50,
Th4;
hence thesis;
end;
now
assume a
<> b & a
<> c & b
<> c;
then
{a, b, c}
in Pl;
then
consider p be
Element of Pl such that
A51: p
=
{a, b, c};
reconsider P = p as
PLANE of S;
b
in p by
A51,
ENUMSET1:def 1;
then
[b, p]
in i2;
then
A52: B
on P;
c
in p by
A51,
ENUMSET1:def 1;
then
[c, p]
in i2;
then
A53: C
on P;
a
in p by
A51,
ENUMSET1:def 1;
then
[a, p]
in i2;
then A
on P;
then
{A, B, C}
on P by
A52,
A53,
Th4;
hence thesis;
end;
hence thesis by
A24,
A29;
end;
A54: for p be
Element of Pl holds
[a, p]
in i2 implies a
in p
proof
let p be
Element of Pl;
assume
[a, p]
in i2;
then
consider b be
Element of
{
0 , 1, 2, 3}, q be
Element of Pl such that
A55:
[a, p]
=
[b, q] and
A56: b
in q;
a
= b by
A55,
XTUPLE_0: 1;
hence thesis by
A55,
A56,
XTUPLE_0: 1;
end;
thus S is
with_<=1_plane_per_3_pts
proof
let A,B,C be
POINT of S, P,Q be
PLANE of S;
assume that
A57: not
{A, B, C} is
linear and
A58:
{A, B, C}
on P and
A59:
{A, B, C}
on Q;
reconsider a = A, b = B, c = C as
Element of
{
0 , 1, 2, 3};
reconsider p = P, q = Q as
Element of Pl;
p
in Pl;
then
consider x1,x2,x3 be
Element of
{
0 , 1, 2, 3} such that
A60: p
=
{x1, x2, x3} and x1
<> x2 and x1
<> x3 and x2
<> x3;
A
on P by
A58,
Th4;
then
[a, p]
in i2;
then a
in p by
A54;
then
A61: a
= x1 or a
= x2 or a
= x3 by
A60,
ENUMSET1:def 1;
C
on P by
A58,
Th4;
then
[c, p]
in i2;
then c
in p by
A54;
then
A62: c
= x1 or c
= x2 or c
= x3 by
A60,
ENUMSET1:def 1;
B
on P by
A58,
Th4;
then
[b, p]
in i2;
then b
in p by
A54;
then
A63: b
= x1 or b
= x2 or b
= x3 by
A60,
ENUMSET1:def 1;
q
in Pl;
then
consider x1,x2,x3 be
Element of
{
0 , 1, 2, 3} such that
A64: q
=
{x1, x2, x3} and x1
<> x2 and x1
<> x3 and x2
<> x3;
B
on Q by
A59,
Th4;
then
[b, q]
in i2;
then b
in q by
A54;
then
A65: b
= x1 or b
= x2 or b
= x3 by
A64,
ENUMSET1:def 1;
A66:
now
consider L be
LINE of S such that
A67:
{A, C}
on L by
A4;
A68: A
on L & C
on L by
A67,
Th1;
consider K be
LINE of S such that
A69:
{A, B}
on K by
A4;
A70: ( not
{A, B, C}
on K) & not
{A, B, C}
on L by
A57;
assume
A71: A
= B or A
= C or B
= C;
A
on K & B
on K by
A69,
Th1;
hence contradiction by
A71,
A68,
A70,
Th2;
end;
C
on Q by
A59,
Th4;
then
[c, q]
in i2;
then c
in q by
A54;
then
A72: c
= x1 or c
= x2 or c
= x3 by
A64,
ENUMSET1:def 1;
A
on Q by
A59,
Th4;
then
[a, q]
in i2;
then a
in q by
A54;
then a
= x1 or a
= x2 or a
= x3 by
A64,
ENUMSET1:def 1;
hence thesis by
A66,
A60,
A61,
A63,
A62,
A64,
A65,
A72,
ENUMSET1: 57,
ENUMSET1: 58,
ENUMSET1: 59,
ENUMSET1: 60;
end;
thus S is
with_lines_inside_planes
proof
let L be
LINE of S, P be
PLANE of S;
given A,B be
POINT of S such that
A73: A
<> B and
A74:
{A, B}
on L and
A75:
{A, B}
on P;
reconsider a = A, b = B as
Element of
{
0 , 1, 2, 3};
reconsider p = P as
Element of Pl;
A
on P by
A75,
Th3;
then
[a, p]
in i2;
then
A76: a
in p by
A54;
reconsider l = L as
Element of Li;
B
on L by
A74,
Th1;
then
[b, l]
in i1;
then
A77: b
in l by
A12;
B
on P by
A75,
Th3;
then
[b, p]
in i2;
then
A78: b
in p by
A54;
A
on L by
A74,
Th1;
then
[a, l]
in i1;
then
A79: a
in l by
A12;
now
let x be
object;
assume
A80: x
in l;
l
in Li;
then
consider x1,x2 be
Element of
{
0 , 1, 2, 3} such that
A81: l
=
{x1, x2} and x1
<> x2;
A82: b
= x1 or b
= x2 by
A77,
A81,
TARSKI:def 2;
a
= x1 or a
= x2 by
A79,
A81,
TARSKI:def 2;
hence x
in p by
A73,
A76,
A78,
A80,
A81,
A82,
TARSKI:def 2;
end;
then l
c= p;
then
[l, p]
in i3;
hence thesis;
end;
thus S is
with_planes_intersecting_in_2_pts
proof
let A be
POINT of S, P,Q be
PLANE of S;
assume that
A83: A
on P and
A84: A
on Q;
reconsider p = P, q = Q as
Element of Pl;
reconsider a = A as
Element of
{
0 , 1, 2, 3};
p
in Pl;
then
consider x1,x2,x3 be
Element of
{
0 , 1, 2, 3} such that
A85: p
=
{x1, x2, x3} and
A86: x1
<> x2 & x1
<> x3 & x2
<> x3;
A87: x1
in p & x2
in p by
A85,
ENUMSET1:def 1;
A88: x3
in p by
A85,
ENUMSET1:def 1;
q
in Pl;
then
consider y1,y2,y3 be
Element of
{
0 , 1, 2, 3} such that
A89: q
=
{y1, y2, y3} and
A90: y1
<> y2 & y1
<> y3 & y2
<> y3;
A91: y1
in q & y2
in q by
A89,
ENUMSET1:def 1;
A92: y3
in q by
A89,
ENUMSET1:def 1;
[a, q]
in i2 by
A84;
then a
in q by
A54;
then a
= y1 or a
= y2 or a
= y3 by
A89,
ENUMSET1:def 1;
then
consider z3,z4 be
Element of
{
0 , 1, 2, 3} such that
A93: z3
in q & z4
in q and
A94: z3
<> a and
A95: z4
<> a & z3
<> z4 by
A90,
A91,
A92;
[a, p]
in i2 by
A83;
then a
in p by
A54;
then a
= x1 or a
= x2 or a
= x3 by
A85,
ENUMSET1:def 1;
then
consider z1,z2 be
Element of
{
0 , 1, 2, 3} such that
A96: z1
in p & z2
in p and
A97: z1
<> a and
A98: z2
<> a and
A99: z1
<> z2 by
A86,
A87,
A88;
now
assume
A100: z1
<> z3 & z1
<> z4 & z2
<> z3 & z2
<> z4;
per cases by
ENUMSET1:def 2;
suppose
A101: a
=
0 ;
then
A102: z3
= 1 or z3
= 2 or z3
= 3 by
A94,
ENUMSET1:def 2;
A103: z2
= 1 or z2
= 2 or z2
= 3 by
A98,
A101,
ENUMSET1:def 2;
z1
= 1 or z1
= 2 or z1
= 3 by
A97,
A101,
ENUMSET1:def 2;
hence contradiction by
A99,
A95,
A100,
A101,
A103,
A102,
ENUMSET1:def 2;
end;
suppose
A104: a
= 1;
then
A105: z3
=
0 or z3
= 2 or z3
= 3 by
A94,
ENUMSET1:def 2;
A106: z2
=
0 or z2
= 2 or z2
= 3 by
A98,
A104,
ENUMSET1:def 2;
z1
=
0 or z1
= 2 or z1
= 3 by
A97,
A104,
ENUMSET1:def 2;
hence contradiction by
A99,
A95,
A100,
A104,
A106,
A105,
ENUMSET1:def 2;
end;
suppose
A107: a
= 2;
then
A108: z3
=
0 or z3
= 1 or z3
= 3 by
A94,
ENUMSET1:def 2;
A109: z2
=
0 or z2
= 1 or z2
= 3 by
A98,
A107,
ENUMSET1:def 2;
z1
=
0 or z1
= 1 or z1
= 3 by
A97,
A107,
ENUMSET1:def 2;
hence contradiction by
A99,
A95,
A100,
A107,
A109,
A108,
ENUMSET1:def 2;
end;
suppose
A110: a
= 3;
then
A111: z3
=
0 or z3
= 1 or z3
= 2 by
A94,
ENUMSET1:def 2;
A112: z2
=
0 or z2
= 1 or z2
= 2 by
A98,
A110,
ENUMSET1:def 2;
z1
=
0 or z1
= 1 or z1
= 2 by
A97,
A110,
ENUMSET1:def 2;
hence contradiction by
A99,
A95,
A100,
A110,
A112,
A111,
ENUMSET1:def 2;
end;
end;
then
consider z be
Element of
{
0 , 1, 2, 3} such that
A113: z
in p & z
in q and
A114: a
<> z by
A96,
A97,
A98,
A93;
reconsider B = z as
POINT of S;
take B;
thus A
<> B by
A114;
[z, p]
in i2 &
[z, q]
in i2 by
A113;
hence thesis;
end;
thus S is
up-3-dimensional
proof
reconsider Three = 3 as
Element of
{
0 , 1, 2, 3} by
ENUMSET1:def 2;
reconsider A = Zero1, B = One, C = Two, D = Three as
POINT of S;
take A, B, C, D;
assume
{A, B, C, D} is
planar;
then
consider P be
PLANE of S such that
A115:
{A, B, C, D}
on P;
reconsider p = P as
Element of Pl;
p
in Pl;
then
consider a, b, c such that
A116: p
=
{a, b, c} and a
<> b and a
<> c and b
<> c;
D
on P by
A115;
then
[Three, p]
in i2;
then
A117: Three
in p by
A54;
C
on P by
A115;
then
[Two, p]
in i2;
then Two
in p by
A54;
then
A118: Two
= a or Two
= b or Two
= c by
A116,
ENUMSET1:def 1;
B
on P by
A115;
then
[One, p]
in i2;
then One
in p by
A54;
then
A119: One
= a or One
= b or One
= c by
A116,
ENUMSET1:def 1;
A
on P by
A115;
then
[Zero1, p]
in i2;
then Zero1
in p by
A54;
then Zero1
= a or Zero1
= b or Zero1
= c by
A116,
ENUMSET1:def 1;
hence contradiction by
A116,
A117,
A119,
A118,
ENUMSET1:def 1;
end;
A120: for p be
Element of Pl, l be
Element of Li holds
[l, p]
in i3 implies l
c= p
proof
let p be
Element of Pl, l be
Element of Li;
assume
[l, p]
in i3;
then
consider k be
Element of Li, q be
Element of Pl such that
A121:
[l, p]
=
[k, q] and
A122: k
c= q;
l
= k by
A121,
XTUPLE_0: 1;
hence thesis by
A121,
A122,
XTUPLE_0: 1;
end;
thus S is
inc-compatible
proof
let A be
POINT of S, L be
LINE of S, P be
PLANE of S;
reconsider a = A as
Element of
{
0 , 1, 2, 3};
reconsider l = L as
Element of Li;
reconsider p = P as
Element of Pl;
assume that
A123: A
on L and
A124: L
on P;
[l, p]
in i3 by
A124;
then
A125: l
c= p by
A120;
[a, l]
in i1 by
A123;
then a
in l by
A12;
then
[a, p]
in i2 by
A125;
hence thesis;
end;
end;
then
IncStruct (#
{
0 , 1, 2, 3}, Li, Pl, i1, i2, i3 #) is
IncSpace-like;
hence thesis;
end;
end
definition
mode
IncSpace is
IncSpace-like
IncStruct;
end
reserve S for
IncSpace;
reserve A,B,C,D,E for
POINT of S;
reserve K,L,L1,L2 for
LINE of S;
reserve P,P1,P2,Q for
PLANE of S;
reserve F for
Subset of the
Points of S;
theorem ::
INCSP_1:14
Th14: F
on L & L
on P implies F
on P by
Def17;
theorem ::
INCSP_1:15
Th15:
{A, A, B} is
linear
proof
consider K such that
A1:
{A, B}
on K by
Def9;
take K;
thus thesis by
A1,
ENUMSET1: 30;
end;
theorem ::
INCSP_1:16
Th16:
{A, A, B, C} is
planar
proof
consider P such that
A1:
{A, B, C}
on P by
Def12;
take P;
thus thesis by
A1,
ENUMSET1: 31;
end;
theorem ::
INCSP_1:17
Th17:
{A, B, C} is
linear implies
{A, B, C, D} is
planar
proof
given L such that
A1:
{A, B, C}
on L;
(
{A, B}
\/
{C})
on L by
A1,
ENUMSET1: 3;
then
A2:
{A, B}
on L by
Th8;
consider P such that
A3:
{A, B, D}
on P by
Def12;
(
{A, B}
\/
{D})
on P by
A3,
ENUMSET1: 3;
then
A4:
{A, B}
on P by
Th11;
assume
A5: not
{A, B, C, D} is
planar;
then A
<> B by
Th16;
then L
on P by
A2,
A4,
Def14;
then
A6:
{A, B, C}
on P by
A1,
Th14;
then
A7: C
on P by
Th4;
A8: D
on P by
A3,
Th4;
A
on P & B
on P by
A6,
Th4;
then
{A, B, C, D}
on P by
A7,
A8,
Th5;
hence contradiction by
A5;
end;
theorem ::
INCSP_1:18
Th18: A
<> B &
{A, B}
on L & not C
on L implies not
{A, B, C} is
linear
proof
assume that
A1: A
<> B &
{A, B}
on L and
A2: not C
on L;
given K such that
A3:
{A, B, C}
on K;
(
{A, B}
\/
{C})
on K by
A3,
ENUMSET1: 3;
then
{A, B}
on K by
Th10;
then L
= K by
A1,
Def10;
hence contradiction by
A2,
A3,
Th2;
end;
theorem ::
INCSP_1:19
Th19: not
{A, B, C} is
linear &
{A, B, C}
on P & not D
on P implies not
{A, B, C, D} is
planar
proof
assume that
A1: ( not
{A, B, C} is
linear) &
{A, B, C}
on P and
A2: not D
on P;
given Q such that
A3:
{A, B, C, D}
on Q;
(
{A, B, C}
\/
{D})
on Q by
A3,
ENUMSET1: 6;
then
{A, B, C}
on Q by
Th9;
then P
= Q by
A1,
Def13;
hence contradiction by
A2,
A3,
Th5;
end;
theorem ::
INCSP_1:20
not (ex P st K
on P & L
on P) implies K
<> L
proof
assume that
A1: not (ex P st K
on P & L
on P) and
A2: K
= L;
consider A, B such that
A3: A
<> B and
A4:
{A, B}
on K by
Def8;
A5: A
on K & B
on K by
A4,
Th1;
consider C, D such that
A6: C
<> D and
A7:
{C, D}
on L by
Def8;
C
on K by
A2,
A7,
Th1;
then
{A, B, C}
on K by
A5,
Th2;
then
{A, B, C} is
linear;
then
{A, B, C, D} is
planar by
Th17;
then
consider Q such that
A8:
{A, B, C, D}
on Q;
C
on Q & D
on Q by
A8,
Th5;
then
{C, D}
on Q by
Th3;
then
A9: L
on Q by
A6,
A7,
Def14;
A
on Q & B
on Q by
A8,
Th5;
then
{A, B}
on Q by
Th3;
then K
on Q by
A3,
A4,
Def14;
hence contradiction by
A1,
A9;
end;
Lm1: ex B st A
<> B & B
on L
proof
consider B, C such that
A1: B
<> C and
A2:
{B, C}
on L by
Def8;
A3: A
<> C or A
<> B by
A1;
B
on L & C
on L by
A2,
Th1;
hence thesis by
A3;
end;
theorem ::
INCSP_1:21
not (ex P st L
on P & L1
on P & L2
on P) & (ex A st A
on L & A
on L1 & A
on L2) implies L
<> L1
proof
assume
A1: not (ex P st L
on P & L1
on P & L2
on P);
given A such that
A2: A
on L and
A3: A
on L1 and
A4: A
on L2;
consider C such that
A5: A
<> C and
A6: C
on L1 by
Lm1;
consider D such that
A7: A
<> D and
A8: D
on L2 by
Lm1;
consider B such that
A9: A
<> B and
A10: B
on L by
Lm1;
assume
A11: L
= L1;
then
{A, C, B}
on L1 by
A3,
A10,
A6,
Th2;
then (
{A, C}
\/
{B})
on L1 by
ENUMSET1: 3;
then
A12:
{A, C}
on L1 by
Th10;
{A, B, C}
on L by
A3,
A11,
A10,
A6,
Th2;
then
{A, B, C} is
linear;
then
{A, B, C, D} is
planar by
Th17;
then
consider Q such that
A13:
{A, B, C, D}
on Q;
A
on Q & D
on Q by
A13,
Th5;
then
A14:
{A, D}
on Q by
Th3;
{A, D}
on L2 by
A4,
A8,
Th1;
then
A15: L2
on Q by
A7,
A14,
Def14;
A
on Q & C
on Q by
A13,
Th5;
then
{A, C}
on Q by
Th3;
then
A16: L1
on Q by
A5,
A12,
Def14;
(
{A, B}
\/
{C, D})
on Q by
A13,
ENUMSET1: 5;
then
A17:
{A, B}
on Q by
Th11;
{A, B}
on L by
A2,
A10,
Th1;
then L
on Q by
A9,
A17,
Def14;
hence contradiction by
A1,
A16,
A15;
end;
theorem ::
INCSP_1:22
L1
on P & L2
on P & not L
on P & L1
<> L2 implies not (ex Q st L
on Q & L1
on Q & L2
on Q)
proof
assume that
A1: L1
on P and
A2: L2
on P and
A3: not L
on P and
A4: L1
<> L2;
consider A, B such that
A5: A
<> B and
A6:
{A, B}
on L1 by
Def8;
A7:
{A, B}
on P by
A1,
A6,
Th14;
consider C,C1 be
POINT of S such that
A8: C
<> C1 and
A9:
{C, C1}
on L2 by
Def8;
A10:
now
assume C
on L1 & C1
on L1;
then
{C, C1}
on L1 by
Th1;
hence contradiction by
A4,
A8,
A9,
Def10;
end;
A11:
{C, C1}
on P by
A2,
A9,
Th14;
then C
on P by
Th3;
then (
{A, B}
\/
{C})
on P by
A7,
Th9;
then
A12:
{A, B, C}
on P by
ENUMSET1: 3;
C1
on P by
A11,
Th3;
then (
{A, B}
\/
{C1})
on P by
A7,
Th9;
then
A13:
{A, B, C1}
on P by
ENUMSET1: 3;
consider D, E such that
A14: D
<> E and
A15:
{D, E}
on L by
Def8;
given Q such that
A16: L
on Q and
A17: L1
on Q and
A18: L2
on Q;
A19:
{A, B}
on Q by
A17,
A6,
Th14;
A20:
{C, C1}
on Q by
A18,
A9,
Th14;
then
A21: C
on Q by
Th3;
A22:
{D, E}
on Q by
A16,
A15,
Th14;
then
A23: D
on Q by
Th3;
then
{C, D}
on Q by
A21,
Th3;
then (
{A, B}
\/
{C, D})
on Q by
A19,
Th11;
then
{A, B, C, D}
on Q by
ENUMSET1: 5;
then
A24:
{A, B, C, D} is
planar;
A25: E
on Q by
A22,
Th3;
then
{C, E}
on Q by
A21,
Th3;
then (
{A, B}
\/
{C, E})
on Q by
A19,
Th11;
then
{A, B, C, E}
on Q by
ENUMSET1: 5;
then
A26:
{A, B, C, E} is
planar;
A27: C1
on Q by
A20,
Th3;
then
{C1, D}
on Q by
A23,
Th3;
then (
{A, B}
\/
{C1, D})
on Q by
A19,
Th11;
then
{A, B, C1, D}
on Q by
ENUMSET1: 5;
then
A28:
{A, B, C1, D} is
planar;
{C1, E}
on Q by
A27,
A25,
Th3;
then (
{A, B}
\/
{C1, E})
on Q by
A19,
Th11;
then
{A, B, C1, E}
on Q by
ENUMSET1: 5;
then
A29:
{A, B, C1, E} is
planar;
not
{D, E}
on P by
A3,
A14,
A15,
Def14;
then not D
on P or not E
on P by
Th3;
hence contradiction by
A5,
A6,
A24,
A26,
A28,
A29,
A10,
A12,
A13,
Th18,
Th19;
end;
theorem ::
INCSP_1:23
Th23: (ex A st A
on K & A
on L) implies ex P st K
on P & L
on P
proof
given A such that
A1: A
on K and
A2: A
on L;
consider C such that
A3: A
<> C and
A4: C
on L by
Lm1;
A5:
{A, C}
on L by
A2,
A4,
Th1;
consider B such that
A6: A
<> B and
A7: B
on K by
Lm1;
consider P such that
A8:
{A, B, C}
on P by
Def12;
take P;
A9: A
on P by
A8,
Th4;
C
on P by
A8,
Th4;
then
A10:
{A, C}
on P by
A9,
Th3;
B
on P by
A8,
Th4;
then
A11:
{A, B}
on P by
A9,
Th3;
{A, B}
on K by
A1,
A7,
Th1;
hence thesis by
A6,
A3,
A5,
A11,
A10,
Def14;
end;
theorem ::
INCSP_1:24
A
<> B implies ex L st for K holds
{A, B}
on K iff K
= L
proof
assume
A1: A
<> B;
consider L such that
A2:
{A, B}
on L by
Def9;
take L;
thus thesis by
A1,
A2,
Def10;
end;
theorem ::
INCSP_1:25
not
{A, B, C} is
linear implies ex P st for Q holds
{A, B, C}
on Q iff P
= Q
proof
assume
A1: not
{A, B, C} is
linear;
consider P such that
A2:
{A, B, C}
on P by
Def12;
take P;
thus thesis by
A1,
A2,
Def13;
end;
theorem ::
INCSP_1:26
Th26: not A
on L implies ex P st for Q holds A
on Q & L
on Q iff P
= Q
proof
assume
A1: not A
on L;
consider B, C such that
A2: B
<> C and
A3:
{B, C}
on L by
Def8;
consider P such that
A4:
{B, C, A}
on P by
Def12;
take P;
let Q;
thus A
on Q & L
on Q implies P
= Q
proof
assume that
A5: A
on Q and
A6: L
on Q;
{B, C}
on Q by
A3,
A6,
Th14;
then B
on Q & C
on Q by
Th3;
then
A7:
{B, C, A}
on Q by
A5,
Th4;
not
{B, C, A} is
linear by
A1,
A2,
A3,
Th18;
hence thesis by
A4,
A7,
Def13;
end;
A8: (
{B, C}
\/
{A})
on P by
A4,
ENUMSET1: 3;
thus thesis by
A2,
A3,
A8,
Def14,
Th9;
end;
theorem ::
INCSP_1:27
Th27: K
<> L & (ex A st A
on K & A
on L) implies ex P st for Q holds K
on Q & L
on Q iff P
= Q
proof
assume that
A1: K
<> L and
A2: ex A st A
on K & A
on L;
consider A such that
A3: A
on K and
A4: A
on L by
A2;
consider C such that
A5: A
<> C and
A6: C
on L by
Lm1;
consider B such that
A7: A
<> B and
A8: B
on K by
Lm1;
consider P such that
A9:
{A, B, C}
on P by
Def12;
A10: A
on P by
A9,
Th4;
take P;
let Q;
thus K
on Q & L
on Q implies P
= Q
proof
{A, C}
on L by
A4,
A6,
Th1;
then not
{A, C}
on K by
A1,
A5,
Def10;
then
A11: not C
on K by
A3,
Th1;
assume that
A12: K
on Q and
A13: L
on Q;
A14: C
on Q by
A6,
A13,
Def17;
A
on Q & B
on Q by
A3,
A8,
A12,
Def17;
then
A15:
{A, B, C}
on Q by
A14,
Th4;
{A, B}
on K by
A3,
A8,
Th1;
then not
{A, B, C} is
linear by
A7,
A11,
Th18;
hence thesis by
A9,
A15,
Def13;
end;
B
on P by
A9,
Th4;
then
A16:
{A, B}
on P by
A10,
Th3;
C
on P by
A9,
Th4;
then
A17:
{A, C}
on P by
A10,
Th3;
A18:
{A, C}
on L by
A4,
A6,
Th1;
{A, B}
on K by
A3,
A8,
Th1;
hence thesis by
A7,
A5,
A18,
A16,
A17,
Def14;
end;
definition
let S;
let A, B;
assume
A1: A
<> B;
::
INCSP_1:def19
func
Line (A,B) ->
LINE of S means
:
Def19:
{A, B}
on it ;
correctness by
A1,
Def9,
Def10;
end
definition
let S;
let A, B, C;
assume
A1: not
{A, B, C} is
linear;
::
INCSP_1:def20
func
Plane (A,B,C) ->
PLANE of S means
:
Def20:
{A, B, C}
on it ;
correctness by
A1,
Def12,
Def13;
end
definition
let S;
let A, L;
assume
A1: not A
on L;
::
INCSP_1:def21
func
Plane (A,L) ->
PLANE of S means
:
Def21: A
on it & L
on it ;
existence
proof
consider B, C such that
A2: B
<> C &
{B, C}
on L by
Def8;
consider P such that
A3:
{B, C, A}
on P by
Def12;
take P;
thus A
on P by
A3,
Th4;
(
{B, C}
\/
{A})
on P by
A3,
ENUMSET1: 3;
then
{B, C}
on P by
Th9;
hence thesis by
A2,
Def14;
end;
uniqueness
proof
let P, Q;
assume that
A4: A
on P & L
on P and
A5: A
on Q & L
on Q;
consider P1 such that
A6: for P2 holds A
on P2 & L
on P2 iff P1
= P2 by
A1,
Th26;
P1
= P by
A4,
A6;
hence thesis by
A5,
A6;
end;
end
definition
let S;
let K, L;
assume that
A1: K
<> L and
A2: ex A st A
on K & A
on L;
::
INCSP_1:def22
func
Plane (K,L) ->
PLANE of S means
:
Def22: K
on it & L
on it ;
existence by
A2,
Th23;
uniqueness
proof
let P, Q;
assume that
A3: K
on P & L
on P and
A4: K
on Q & L
on Q;
consider P1 such that
A5: for P2 holds K
on P2 & L
on P2 iff P1
= P2 by
A1,
A2,
Th27;
P
= P1 by
A3,
A5;
hence thesis by
A4,
A5;
end;
end
theorem ::
INCSP_1:28
A
<> B implies (
Line (A,B))
= (
Line (B,A))
proof
assume
A1: A
<> B;
then
{A, B}
on (
Line (A,B)) by
Def19;
hence thesis by
A1,
Def19;
end;
theorem ::
INCSP_1:29
Th29: not
{A, B, C} is
linear implies (
Plane (A,B,C))
= (
Plane (A,C,B))
proof
assume
A1: not
{A, B, C} is
linear;
then not
{A, C, B} is
linear by
ENUMSET1: 57;
then
{A, C, B}
on (
Plane (A,C,B)) by
Def20;
then
{A, B, C}
on (
Plane (A,C,B)) by
ENUMSET1: 57;
hence thesis by
A1,
Def20;
end;
theorem ::
INCSP_1:30
Th30: not
{A, B, C} is
linear implies (
Plane (A,B,C))
= (
Plane (B,A,C))
proof
assume
A1: not
{A, B, C} is
linear;
then not
{B, A, C} is
linear by
ENUMSET1: 58;
then
{B, A, C}
on (
Plane (B,A,C)) by
Def20;
then
{A, B, C}
on (
Plane (B,A,C)) by
ENUMSET1: 58;
hence thesis by
A1,
Def20;
end;
theorem ::
INCSP_1:31
not
{A, B, C} is
linear implies (
Plane (A,B,C))
= (
Plane (B,C,A))
proof
assume
A1: not
{A, B, C} is
linear;
then
A2: not
{B, C, A} is
linear by
ENUMSET1: 59;
thus (
Plane (A,B,C))
= (
Plane (B,A,C)) by
A1,
Th30
.= (
Plane (B,C,A)) by
A2,
Th29;
end;
theorem ::
INCSP_1:32
Th32: not
{A, B, C} is
linear implies (
Plane (A,B,C))
= (
Plane (C,A,B))
proof
assume
A1: not
{A, B, C} is
linear;
then
A2: not
{C, A, B} is
linear by
ENUMSET1: 59;
thus (
Plane (A,B,C))
= (
Plane (A,C,B)) by
A1,
Th29
.= (
Plane (C,A,B)) by
A2,
Th30;
end;
theorem ::
INCSP_1:33
not
{A, B, C} is
linear implies (
Plane (A,B,C))
= (
Plane (C,B,A))
proof
assume
A1: not
{A, B, C} is
linear;
then
A2: not
{C, B, A} is
linear by
ENUMSET1: 60;
thus (
Plane (A,B,C))
= (
Plane (C,A,B)) by
A1,
Th32
.= (
Plane (C,B,A)) by
A2,
Th29;
end;
theorem ::
INCSP_1:34
K
<> L & (ex A st A
on K & A
on L) implies (
Plane (K,L))
= (
Plane (L,K))
proof
assume
A1: K
<> L;
set P2 = (
Plane (L,K));
set P1 = (
Plane (K,L));
given A such that
A2: A
on K and
A3: A
on L;
consider C such that
A4: A
<> C and
A5: C
on L by
Lm1;
consider B such that
A6: A
<> B and
A7: B
on K by
Lm1;
A8: K
on P2 by
A1,
A2,
A3,
Def22;
then
A9: B
on P2 by
A7,
Def17;
A10: K
on P1 by
A1,
A2,
A3,
Def22;
then
A11: B
on P1 by
A7,
Def17;
A12:
now
assume
{A, B, C} is
linear;
then
consider L1 such that
A13:
{A, B, C}
on L1;
A14: A
on L1 by
A13,
Th2;
C
on L1 by
A13,
Th2;
then
A15:
{A, C}
on L1 by
A14,
Th1;
A16:
{A, B}
on K by
A2,
A7,
Th1;
B
on L1 by
A13,
Th2;
then
{A, B}
on L1 by
A14,
Th1;
then
A17: K
= L1 by
A6,
A16,
Def10;
{A, C}
on L by
A3,
A5,
Th1;
hence contradiction by
A1,
A4,
A15,
A17,
Def10;
end;
L
on P2 by
A1,
A2,
A3,
Def22;
then
A18: C
on P2 by
A5,
Def17;
A
on P2 by
A2,
A8,
Def17;
then
A19:
{A, B, C}
on P2 by
A9,
A18,
Th4;
L
on P1 by
A1,
A2,
A3,
Def22;
then
A20: C
on P1 by
A5,
Def17;
A
on P1 by
A2,
A10,
Def17;
then
{A, B, C}
on P1 by
A11,
A20,
Th4;
hence thesis by
A19,
A12,
Def13;
end;
theorem ::
INCSP_1:35
Th35: A
<> B & C
on (
Line (A,B)) implies
{A, B, C} is
linear
proof
assume A
<> B;
then
{A, B}
on (
Line (A,B)) by
Def19;
then
A1: A
on (
Line (A,B)) & B
on (
Line (A,B)) by
Th1;
assume C
on (
Line (A,B));
then
{A, B, C}
on (
Line (A,B)) by
A1,
Th2;
hence thesis;
end;
theorem ::
INCSP_1:36
A
<> B & A
<> C &
{A, B, C} is
linear implies (
Line (A,B))
= (
Line (A,C))
proof
assume
A1: A
<> B;
then
A2:
{A, B}
on (
Line (A,B)) by
Def19;
then
A3: A
on (
Line (A,B)) by
Th1;
assume
A4: A
<> C;
assume
{A, B, C} is
linear;
then C
on (
Line (A,B)) by
A1,
A2,
Th18;
then
{A, C}
on (
Line (A,B)) by
A3,
Th1;
hence thesis by
A4,
Def19;
end;
theorem ::
INCSP_1:37
not
{A, B, C} is
linear implies (
Plane (A,B,C))
= (
Plane (C,(
Line (A,B))))
proof
assume
A1: not
{A, B, C} is
linear;
then A
<> B by
Th15;
then
A2:
{A, B}
on (
Line (A,B)) by
Def19;
then A
on (
Line (A,B)) & B
on (
Line (A,B)) by
Th1;
then
A3: C
on (
Line (A,B)) implies
{A, B, C}
on (
Line (A,B)) by
Th2;
then (
Line (A,B))
on (
Plane (C,(
Line (A,B)))) by
A1,
Def21;
then
A4:
{A, B}
on (
Plane (C,(
Line (A,B)))) by
A2,
Th14;
C
on (
Plane (C,(
Line (A,B)))) by
A1,
A3,
Def21;
then (
{A, B}
\/
{C})
on (
Plane (C,(
Line (A,B)))) by
A4,
Th9;
then
{A, B, C}
on (
Plane (C,(
Line (A,B)))) by
ENUMSET1: 3;
hence thesis by
A1,
Def20;
end;
theorem ::
INCSP_1:38
not
{A, B, C} is
linear & D
on (
Plane (A,B,C)) implies
{A, B, C, D} is
planar
proof
assume that
A1: not
{A, B, C} is
linear and
A2: D
on (
Plane (A,B,C));
{A, B, C}
on (
Plane (A,B,C)) by
A1,
Def20;
then (
{A, B, C}
\/
{D})
on (
Plane (A,B,C)) by
A2,
Th9;
then
{A, B, C, D}
on (
Plane (A,B,C)) by
ENUMSET1: 6;
hence thesis;
end;
theorem ::
INCSP_1:39
not C
on L &
{A, B}
on L & A
<> B implies (
Plane (C,L))
= (
Plane (A,B,C))
proof
assume that
A1: not C
on L and
A2:
{A, B}
on L and
A3: A
<> B;
set P1 = (
Plane (C,L));
L
on P1 by
A1,
Def21;
then
A4:
{A, B}
on P1 by
A2,
Th14;
C
on P1 by
A1,
Def21;
then (
{A, B}
\/
{C})
on P1 by
A4,
Th9;
then
A5:
{A, B, C}
on P1 by
ENUMSET1: 3;
not
{A, B, C} is
linear by
A1,
A2,
A3,
Th18;
hence thesis by
A5,
Def20;
end;
theorem ::
INCSP_1:40
not
{A, B, C} is
linear implies (
Plane (A,B,C))
= (
Plane ((
Line (A,B)),(
Line (A,C))))
proof
set P2 = (
Plane ((
Line (A,B)),(
Line (A,C))));
set L1 = (
Line (A,B));
set L2 = (
Line (A,C));
assume
A1: not
{A, B, C} is
linear;
then
A2: A
<> B by
Th15;
then
A3:
{A, B}
on L1 by
Def19;
then
A4: A
on L1 by
Th1;
not
{A, C, B} is
linear by
A1,
ENUMSET1: 57;
then
A5: A
<> C by
Th15;
then
A6:
{A, C}
on L2 by
Def19;
then
A7: A
on L2 by
Th1;
{A, C}
on L2 by
A5,
Def19;
then C
on L2 by
Th1;
then
A8: L1
<> L2 by
A1,
A2,
Th35;
then L2
on P2 by
A4,
A7,
Def22;
then
{A, C}
on P2 by
A6,
Th14;
then
A9: C
on P2 by
Th3;
L1
on P2 by
A4,
A7,
A8,
Def22;
then
{A, B}
on P2 by
A3,
Th14;
then (
{A, B}
\/
{C})
on P2 by
A9,
Th9;
then
{A, B, C}
on P2 by
ENUMSET1: 3;
hence thesis by
A1,
Def20;
end;
Lm2: ex A, B, C, D st A
on P & not
{A, B, C, D} is
planar
proof
consider A such that
A1: A
on P by
Def11;
consider A1,B1,C1,D1 be
POINT of S such that
A2: not
{A1, B1, C1, D1} is
planar by
Def16;
now
assume
A3: not A1
on P;
A4:
now
A5: A1
<> B1 by
A2,
Th16;
then
A6:
{A1, B1}
on (
Line (A1,B1)) by
Def19;
{A1, B1}
on (
Line (A1,B1)) by
A5,
Def19;
then C1
on (
Line (A1,B1)) implies (
{A1, B1}
\/
{C1})
on (
Line (A1,B1)) by
Th8;
then
A7: C1
on (
Line (A1,B1)) implies
{A1, B1, C1}
on (
Line (A1,B1)) by
ENUMSET1: 3;
set Q = (
Plane (A1,B1,C1));
assume
A8: A
on (
Line (A1,B1));
A9: not
{A1, B1, C1} is
linear by
A2,
Th17;
then
{A1, B1, C1}
on Q by
Def20;
then
A10: A1
on Q & C1
on Q by
Th4;
A11:
{A1, B1, C1}
on Q by
A9,
Def20;
then D1
on Q implies (
{A1, B1, C1}
\/
{D1})
on Q by
Th9;
then
A12: D1
on Q implies
{A1, B1, C1, D1}
on Q by
ENUMSET1: 6;
(
{A1, B1}
\/
{C1})
on Q by
A11,
ENUMSET1: 3;
then
{A1, B1}
on Q by
Th11;
then (
Line (A1,B1))
on Q by
A5,
A6,
Def14;
then A
on Q by
A8,
Def17;
then
A13:
{A, A1, C1}
on (
Plane (A1,B1,C1)) by
A10,
Th4;
A1
on (
Line (A1,B1)) by
A6,
Th1;
then
{A, A1}
on (
Line (A1,B1)) by
A8,
Th1;
then not
{A, A1, C1} is
linear by
A1,
A3,
A9,
A7,
Th18;
then not
{A, A1, C1, D1} is
planar by
A2,
A12,
A13,
Th19;
hence thesis by
A1;
end;
now
set Q = (
Plane (A1,B1,A));
assume
A14: not A
on (
Line (A1,B1));
A15: A1
<> B1 by
A2,
Th16;
then
A16:
{A1, B1}
on (
Line (A1,B1)) by
Def19;
then not
{A1, B1, A} is
linear by
A14,
A15,
Th18;
then
A17:
{A1, B1, A}
on Q by
Def20;
then (
{A1, B1}
\/
{A})
on Q by
ENUMSET1: 3;
then
{A1, B1}
on Q by
Th9;
then
{C1, D1}
on Q implies (
{A1, B1}
\/
{C1, D1})
on Q by
Th11;
then
{C1, D1}
on Q implies
{A1, B1, C1, D1}
on Q by
ENUMSET1: 5;
then not C1
on Q or not D1
on Q by
A2,
Th3;
then not
{A1, B1, A, C1} is
planar or not
{A1, B1, A, D1} is
planar by
A14,
A15,
A16,
A17,
Th18,
Th19;
then not
{A, A1, B1, C1} is
planar or not
{A, A1, B1, D1} is
planar by
ENUMSET1: 67;
hence thesis by
A1;
end;
hence thesis by
A4;
end;
hence thesis by
A2;
end;
theorem ::
INCSP_1:41
Th41: ex A, B, C st
{A, B, C}
on P & not
{A, B, C} is
linear
proof
consider A1,B1,C1,D1 be
POINT of S such that
A1: A1
on P and
A2: not
{A1, B1, C1, D1} is
planar by
Lm2;
not
{B1, D1, A1, C1} is
planar by
A2,
ENUMSET1: 69;
then
A3: B1
<> D1 by
Th16;
not
{C1, D1, A1, B1} is
planar by
A2,
ENUMSET1: 73;
then
A4: C1
<> D1 by
Th16;
not
{A1, B1, C1, D1}
on P by
A2;
then not
{B1, C1, D1, A1}
on P by
ENUMSET1: 68;
then not (
{B1, C1, D1}
\/
{A1})
on P by
ENUMSET1: 6;
then not
{B1, C1, D1}
on P by
A1,
Th9;
then not B1
on P or not C1
on P or not D1
on P by
Th4;
then
consider X be
POINT of S such that
A5: X
= B1 or X
= C1 or X
= D1 and
A6: not X
on P;
not
{B1, C1, A1, D1} is
planar by
A2,
ENUMSET1: 67;
then B1
<> C1 by
Th16;
then
consider Y,Z be
POINT of S such that
A7: (Y
= B1 or Y
= C1 or Y
= D1) & (Z
= B1 or Z
= C1 or Z
= D1) & Y
<> X & Z
<> X & Y
<> Z by
A5,
A3,
A4;
set P1 = (
Plane (X,Y,A1)), P2 = (
Plane (X,Z,A1));
A8:
now
assume
{A1, X, Y, Z} is
planar;
then
{A1, D1, B1, C1} is
planar or
{A1, D1, C1, B1} is
planar by
A2,
A5,
A7,
ENUMSET1: 62;
hence contradiction by
A2,
ENUMSET1: 63,
ENUMSET1: 64;
end;
then not
{A1, X, Y} is
linear by
Th17;
then not
{X, Y, A1} is
linear by
ENUMSET1: 59;
then
A9:
{X, Y, A1}
on P1 by
Def20;
then
A10: A1
on P1 by
Th4;
then
consider B such that
A11: A1
<> B and
A12: B
on P1 and
A13: B
on P by
A1,
Def15;
not
{X, Z, A1, Y} is
planar by
A8,
ENUMSET1: 69;
then not
{X, Z, A1} is
linear by
Th17;
then
A14:
{X, Z, A1}
on P2 by
Def20;
then
A15: A1
on P2 by
Th4;
then
consider C such that
A16: A1
<> C and
A17: C
on P and
A18: C
on P2 by
A1,
Def15;
take A1, B, C;
thus
{A1, B, C}
on P by
A1,
A13,
A17,
Th4;
given K such that
A19:
{A1, B, C}
on K;
A20:
{A1, C}
on P2 by
A15,
A18,
Th3;
{A1, C, B}
on K by
A19,
ENUMSET1: 57;
then (
{A1, C}
\/
{B})
on K by
ENUMSET1: 3;
then
{A1, C}
on K by
Th10;
then
A21: K
on P2 by
A16,
A20,
Def14;
consider E such that
A22: B
<> E and
A23: E
on K by
Lm1;
(
{A1, B}
\/
{C})
on K by
A19,
ENUMSET1: 3;
then
A24:
{A1, B}
on K by
Th10;
A25:
now
{A1, B}
on P by
A1,
A13,
Th3;
then K
on P by
A11,
A24,
Def14;
then E
on P by
A23,
Def17;
then
A26:
{E, B}
on P by
A13,
Th3;
assume
{X, B, E} is
linear;
then
consider L such that
A27:
{X, B, E}
on L;
A28: X
on L by
A27,
Th2;
{E, B, X}
on L by
A27,
ENUMSET1: 60;
then (
{E, B}
\/
{X})
on L by
ENUMSET1: 3;
then
{E, B}
on L by
Th8;
then L
on P by
A22,
A26,
Def14;
hence contradiction by
A6,
A28,
Def17;
end;
B
on K by
A19,
Th2;
then
A29: B
on P2 by
A21,
Def17;
A30: X
on P2 by
A14,
Th4;
A31: X
on P1 by
A9,
Th4;
{A1, B}
on P1 by
A10,
A12,
Th3;
then K
on P1 by
A11,
A24,
Def14;
then E
on P1 by
A23,
Def17;
then
A32:
{X, B, E}
on P1 by
A12,
A31,
Th4;
E
on P2 by
A23,
A21,
Def17;
then
{X, B, E}
on P2 by
A29,
A30,
Th4;
then P1
= P2 by
A25,
A32,
Def13;
then Z
on P1 by
A14,
Th4;
then (
{X, Y, A1}
\/
{Z})
on P1 by
A9,
Th9;
then
{X, Y, A1, Z}
on P1 by
ENUMSET1: 6;
then
{X, Y, A1, Z} is
planar;
hence contradiction by
A8,
ENUMSET1: 67;
end;
theorem ::
INCSP_1:42
ex A, B, C, D st A
on P & not
{A, B, C, D} is
planar by
Lm2;
theorem ::
INCSP_1:43
ex B st A
<> B & B
on L by
Lm1;
theorem ::
INCSP_1:44
Th44: A
<> B implies ex C st C
on P & not
{A, B, C} is
linear
proof
consider L such that
A1:
{A, B}
on L by
Def9;
consider C, D, E such that
A2:
{C, D, E}
on P and
A3: not
{C, D, E} is
linear by
Th41;
A4: C
on P & D
on P by
A2,
Th4;
not
{C, D, E}
on L by
A3;
then
A5: not C
on L or not D
on L or not E
on L by
Th2;
A6: E
on P by
A2,
Th4;
assume A
<> B;
then not
{A, B, C} is
linear or not
{A, B, D} is
linear or not
{A, B, E} is
linear by
A1,
A5,
Th18;
hence thesis by
A4,
A6;
end;
theorem ::
INCSP_1:45
Th45: not
{A, B, C} is
linear implies ex D st not
{A, B, C, D} is
planar
proof
assume
A1: not
{A, B, C} is
linear;
consider P such that
A2:
{A, B, C}
on P by
Def12;
consider A1,B1,C1,D1 be
POINT of S such that
A3: not
{A1, B1, C1, D1} is
planar by
Def16;
not
{A1, B1, C1, D1}
on P by
A3;
then not A1
on P or not B1
on P or not C1
on P or not D1
on P by
Th5;
then not
{A, B, C, A1} is
planar or not
{A, B, C, B1} is
planar or not
{A, B, C, C1} is
planar or not
{A, B, C, D1} is
planar by
A1,
A2,
Th19;
hence thesis;
end;
theorem ::
INCSP_1:46
Th46: ex B, C st
{B, C}
on P & not
{A, B, C} is
linear
proof
A1:
now
assume
A2: not A
on P;
consider B, C, D such that
A3:
{B, C, D}
on P and
A4: not
{B, C, D} is
linear by
Th41;
A5: B
<> C by
A4,
Th15;
take B, C;
(
{B, C}
\/
{D})
on P by
A3,
ENUMSET1: 3;
hence
A6:
{B, C}
on P by
Th9;
assume
{A, B, C} is
linear;
then
consider K such that
A7:
{A, B, C}
on K;
{B, C, A}
on K by
A7,
ENUMSET1: 59;
then
A8: (
{B, C}
\/
{A})
on K by
ENUMSET1: 3;
then
A9: A
on K by
Th8;
{B, C}
on K by
A8,
Th10;
then K
on P by
A6,
A5,
Def14;
hence contradiction by
A2,
A9,
Def17;
end;
now
assume A
on P;
then
consider B such that
A10: A
<> B and
A11: B
on P and B
on P by
Def15;
consider C such that
A12: C
on P and
A13: not
{A, B, C} is
linear by
A10,
Th44;
{B, C}
on P by
A11,
A12,
Th3;
hence thesis by
A13;
end;
hence thesis by
A1;
end;
theorem ::
INCSP_1:47
Th47: A
<> B implies ex C, D st not
{A, B, C, D} is
planar
proof
set P = the
PLANE of S;
assume A
<> B;
then
consider C such that C
on P and
A1: not
{A, B, C} is
linear by
Th44;
ex D st not
{A, B, C, D} is
planar by
A1,
Th45;
hence thesis;
end;
theorem ::
INCSP_1:48
ex B, C, D st not
{A, B, C, D} is
planar
proof
set L = the
LINE of S;
consider B such that
A1: A
<> B and B
on L by
Lm1;
ex C, D st not
{A, B, C, D} is
planar by
A1,
Th47;
hence thesis;
end;
theorem ::
INCSP_1:49
ex L st not A
on L & L
on P
proof
consider B, C such that
A1:
{B, C}
on P and
A2: not
{A, B, C} is
linear by
Th46;
consider L such that
A3:
{B, C}
on L by
Def9;
take L;
A
on L implies (
{B, C}
\/
{A})
on L by
A3,
Th8;
then A
on L implies
{B, C, A}
on L by
ENUMSET1: 3;
then A
on L implies
{A, B, C}
on L by
ENUMSET1: 59;
hence not A
on L by
A2;
not
{B, C, A} is
linear by
A2,
ENUMSET1: 59;
then B
<> C by
Th15;
hence thesis by
A1,
A3,
Def14;
end;
theorem ::
INCSP_1:50
Th50: A
on P implies ex L, L1, L2 st L1
<> L2 & L1
on P & L2
on P & not L
on P & A
on L & A
on L1 & A
on L2
proof
consider B, C such that
A1:
{B, C}
on P and
A2: not
{A, B, C} is
linear by
Th46;
consider D such that
A3: not
{A, B, C, D} is
planar by
A2,
Th45;
assume A
on P;
then
A4: (
{A}
\/
{B, C})
on P by
A1,
Th9;
then
A5:
{A, B, C}
on P by
ENUMSET1: 2;
take L3 = (
Line (A,D)), L1 = (
Line (A,B)), L2 = (
Line (A,C));
A6: A
<> B by
A2,
Th15;
then
A7:
{A, B}
on L1 by
Def19;
A8: not
{A, C, B} is
linear by
A2,
ENUMSET1: 57;
then
A9: A
<> C by
Th15;
then
A10:
{A, C}
on L2 by
Def19;
then B
on L2 implies (
{A, C}
\/
{B})
on L2 by
Th8;
then B
on L2 implies
{A, C, B}
on L2 by
ENUMSET1: 3;
hence L1
<> L2 by
A8,
A7,
Th1;
(
{A, B}
\/
{C})
on P by
A5,
ENUMSET1: 3;
then
{A, B}
on P by
Th11;
hence L1
on P by
A6,
A7,
Def14;
{A, C, B}
on P by
A4,
ENUMSET1: 2;
then (
{A, C}
\/
{B})
on P by
ENUMSET1: 3;
then
{A, C}
on P by
Th9;
hence L2
on P by
A9,
A10,
Def14;
not
{A, D, B, C} is
planar by
A3,
ENUMSET1: 63;
then A
<> D by
Th16;
then
A11:
{A, D}
on L3 by
Def19;
then L3
on P implies
{A, D}
on P by
Th14;
then L3
on P implies D
on P by
Th3;
then L3
on P implies (
{A, B, C}
\/
{D})
on P by
A5,
Th9;
then L3
on P implies
{A, B, C, D}
on P by
ENUMSET1: 6;
hence not L3
on P by
A3;
thus thesis by
A10,
A7,
A11,
Th1;
end;
theorem ::
INCSP_1:51
ex L, L1, L2 st A
on L & A
on L1 & A
on L2 & not (ex P st L
on P & L1
on P & L2
on P)
proof
consider P such that
A1:
{A, A, A}
on P by
Def12;
A
on P by
A1,
Th4;
then
consider L, L1, L2 such that
A2: L1
<> L2 and
A3: L1
on P and
A4: L2
on P and
A5: not L
on P and
A6: A
on L and
A7: A
on L1 and
A8: A
on L2 by
Th50;
consider B such that
A9: A
<> B and
A10: B
on L1 by
Lm1;
consider C such that
A11: A
<> C and
A12: C
on L2 by
Lm1;
A13: C
on P by
A4,
A12,
Def17;
A14:
{A, B}
on L1 by
A7,
A10,
Th1;
then
{A, B}
on P by
A3,
Th14;
then (
{A, B}
\/
{C})
on P by
A13,
Th9;
then
A15:
{A, B, C}
on P by
ENUMSET1: 3;
take L, L1, L2;
thus A
on L & A
on L1 & A
on L2 by
A6,
A7,
A8;
given Q such that
A16: L
on Q and
A17: L1
on Q and
A18: L2
on Q;
A19: C
on Q by
A18,
A12,
Def17;
A20:
{A, C}
on L2 by
A8,
A12,
Th1;
now
given K such that
A21:
{A, B, C}
on K;
{A, C, B}
on K by
A21,
ENUMSET1: 57;
then (
{A, C}
\/
{B})
on K by
ENUMSET1: 3;
then
A22:
{A, C}
on K by
Th8;
(
{A, B}
\/
{C})
on K by
A21,
ENUMSET1: 3;
then
{A, B}
on K by
Th8;
then K
= L1 by
A9,
A14,
Def10;
hence contradiction by
A2,
A11,
A20,
A22,
Def10;
end;
then
A23: not
{A, B, C} is
linear;
{A, B}
on Q by
A17,
A14,
Th14;
then (
{A, B}
\/
{C})
on Q by
A19,
Th9;
then
{A, B, C}
on Q by
ENUMSET1: 3;
hence contradiction by
A5,
A16,
A15,
A23,
Def13;
end;
theorem ::
INCSP_1:52
ex P st A
on P & not L
on P
proof
consider B such that
A1: A
<> B and
A2: B
on L by
Lm1;
consider C, D such that
A3: not
{A, B, C, D} is
planar by
A1,
Th47;
take P = (
Plane (A,C,D));
A4: not
{A, C, D, B} is
planar by
A3,
ENUMSET1: 63;
then not
{A, C, D} is
linear by
Th17;
then
A5:
{A, C, D}
on P by
Def20;
hence A
on P by
Th4;
B
on P implies (
{A, C, D}
\/
{B})
on P by
A5,
Th9;
then B
on P implies
{A, C, D, B}
on P by
ENUMSET1: 6;
hence thesis by
A2,
A4,
Def17;
end;
theorem ::
INCSP_1:53
ex A st A
on P & not A
on L
proof
consider A, B such that
A1: A
<> B and
A2:
{A, B}
on L by
Def8;
consider C such that
A3: C
on P and
A4: not
{A, B, C} is
linear by
A1,
Th44;
take C;
thus C
on P by
A3;
C
on L implies (
{A, B}
\/
{C})
on L by
A2,
Th8;
then C
on L implies
{A, B, C}
on L by
ENUMSET1: 3;
hence thesis by
A4;
end;
theorem ::
INCSP_1:54
ex K st not (ex P st L
on P & K
on P)
proof
consider A, B such that
A1: A
<> B and
A2:
{A, B}
on L by
Def8;
consider C, D such that
A3: not
{A, B, C, D} is
planar by
A1,
Th47;
take K = (
Line (C,D));
given P such that
A4: L
on P and
A5: K
on P;
not
{C, D, A, B} is
planar by
A3,
ENUMSET1: 73;
then C
<> D by
Th16;
then
{C, D}
on K by
Def19;
then
A6:
{C, D}
on P by
A5,
Th14;
{A, B}
on P by
A2,
A4,
Th14;
then (
{A, B}
\/
{C, D})
on P by
A6,
Th11;
then
{A, B, C, D}
on P by
ENUMSET1: 5;
hence thesis by
A3;
end;
theorem ::
INCSP_1:55
ex P, Q st P
<> Q & L
on P & L
on Q
proof
consider A, B such that
A1: A
<> B and
A2:
{A, B}
on L by
Def8;
consider C, D such that
A3: not
{A, B, C, D} is
planar by
A1,
Th47;
take P = (
Plane (A,B,C)), Q = (
Plane (A,B,D));
not
{A, B, C} is
linear by
A3,
Th17;
then
A4:
{A, B, C}
on P by
Def20;
not
{A, B, D, C} is
planar by
A3,
ENUMSET1: 61;
then not
{A, B, D} is
linear by
Th17;
then
A5:
{A, B, D}
on Q by
Def20;
then (
{A, B}
\/
{D})
on Q by
ENUMSET1: 3;
then
A6:
{A, B}
on Q by
Th11;
D
on Q by
A5,
Th4;
then P
= Q implies (
{A, B, C}
\/
{D})
on P by
A4,
Th9;
then P
= Q implies
{A, B, C, D}
on P by
ENUMSET1: 6;
hence P
<> Q by
A3;
(
{A, B}
\/
{C})
on P by
A4,
ENUMSET1: 3;
then
{A, B}
on P by
Th11;
hence thesis by
A1,
A2,
A6,
Def14;
end;
theorem ::
INCSP_1:56
not L
on P &
{A, B}
on L &
{A, B}
on P implies A
= B by
Def14;
theorem ::
INCSP_1:57
P
<> Q implies not (ex A st A
on P & A
on Q) or ex L st for B holds B
on P & B
on Q iff B
on L
proof
assume
A1: P
<> Q;
given A such that
A2: A
on P and
A3: A
on Q;
consider C such that
A4: A
<> C and
A5: C
on P and
A6: C
on Q by
A2,
A3,
Def15;
take L = (
Line (A,C));
A7:
{A, C}
on L by
A4,
Def19;
{A, C}
on Q by
A3,
A6,
Th3;
then
A8: L
on Q by
A4,
A7,
Def14;
let B;
{A, C}
on P by
A2,
A5,
Th3;
then
A9: L
on P by
A4,
A7,
Def14;
thus B
on P & B
on Q implies B
on L
proof
assume that
A10: B
on P and
A11: B
on Q and
A12: not B
on L;
consider P1 such that
A13: for P2 holds B
on P2 & L
on P2 iff P1
= P2 by
A12,
Th26;
P
= P1 by
A9,
A10,
A13;
hence contradiction by
A1,
A8,
A11,
A13;
end;
thus thesis by
A9,
A8,
Def17;
end;