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, b is Element of {0,1,2,3} : a <> b }
;
then reconsider Li = { {a,b} where a, b is Element of {0,1,2,3} : a <> b } as non empty set ;
{Zero1,One,Two} in { {a,b,c} where a, b, c is Element of {0,1,2,3} : ( a <> b & a <> c & b <> c ) }
;
then reconsider Pl = { {a,b,c} where a, b, c is Element of {0,1,2,3} : ( a <> b & a <> c & b <> c ) } as non empty set ;
{ [a,l] where a is Element of {0,1,2,3}, l is Element of Li : a in l } c= [:{0,1,2,3},Li:]
proof
let x be
object ;
TARSKI:def 3 ( not x in { [a,l] where a is Element of {0,1,2,3}, l is Element of Li : a in l } or x in [:{0,1,2,3},Li:] )
assume
x in { [a,l] where a is Element of {0,1,2,3}, l is Element of Li : a in l }
;
x in [:{0,1,2,3},Li:]
then
ex
a being
Element of
{0,1,2,3} ex
l being
Element of
Li st
(
x = [a,l] &
a in l )
;
hence
x in [:{0,1,2,3},Li:]
;
verum
end;
then reconsider i1 = { [a,l] where a is Element of {0,1,2,3}, l is Element of Li : a in l } as Relation of {0,1,2,3},Li ;
{ [a,p] where a is Element of {0,1,2,3}, p is Element of Pl : a in p } c= [:{0,1,2,3},Pl:]
proof
let x be
object ;
TARSKI:def 3 ( not x in { [a,p] where a is Element of {0,1,2,3}, p is Element of Pl : a in p } or x in [:{0,1,2,3},Pl:] )
assume
x in { [a,p] where a is Element of {0,1,2,3}, p is Element of Pl : a in p }
;
x in [:{0,1,2,3},Pl:]
then
ex
a being
Element of
{0,1,2,3} ex
p being
Element of
Pl st
(
x = [a,p] &
a in p )
;
hence
x in [:{0,1,2,3},Pl:]
;
verum
end;
then reconsider i2 = { [a,p] where a is Element of {0,1,2,3}, p is Element of Pl : a in p } as Relation of {0,1,2,3},Pl ;
{ [l,p] where l is Element of Li, p is Element of Pl : l c= p } c= [:Li,Pl:]
then reconsider i3 = { [l,p] where l is Element of Li, p is Element of Pl : l c= p } as Relation of Li,Pl ;
now ( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_non-trivial_lines & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is linear & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-2-rank & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_non-empty_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is planar & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_<=1_plane_per_3_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )set S =
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
with_non-trivial_lines
( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is linear & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-2-rank & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_non-empty_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is planar & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_<=1_plane_per_3_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )proof
let L be
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 8 ex A, B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st
( A <> B & {A,B} on L )
reconsider l =
L as
Element of
Li ;
l in Li
;
then consider a,
b being
Element of
{0,1,2,3} such that A1:
l = {a,b}
and A2:
a <> b
;
reconsider A =
a,
B =
b as
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
take
A
;
ex B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st
( A <> B & {A,B} on L )
take
B
;
( A <> B & {A,B} on L )
thus
A <> B
by A2;
{A,B} on L
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
{A,B} on L
by A3, Th1;
verum
end; thus A4:
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
linear
( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-2-rank & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_non-empty_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is planar & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_<=1_plane_per_3_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )proof
let A,
B be
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 9 ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L
reconsider a =
A,
b =
B as
Element of
{0,1,2,3} ;
A5:
now ( a = b implies ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L )
for
a being
Element of
{0,1,2,3} ex
c being
Element of
{0,1,2,3} st
a <> c
proof
let a be
Element of
{0,1,2,3};
ex c being Element of {0,1,2,3} st a <> c
A6:
now ( ( a = 1 or a = 2 or a = 3 ) implies ex c being Element of {0,1,2,3} st a <> c )assume
(
a = 1 or
a = 2 or
a = 3 )
;
ex c being Element of {0,1,2,3} st a <> cthen
a <> Zero1
;
hence
ex
c being
Element of
{0,1,2,3} st
a <> c
;
verum end;
hence
ex
c being
Element of
{0,1,2,3} st
a <> c
by A6, ENUMSET1:def 2;
verum
end; then consider c being
Element of
{0,1,2,3} such that A7:
a <> c
;
{a,c} in Li
by A7;
then consider l being
Element of
Li such that A8:
l = {a,c}
;
reconsider L =
l as
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
a in l
by A8, TARSKI:def 2;
then
[a,l] in i1
;
then A9:
A on L
;
assume
a = b
;
ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on Lthen
{A,B} on L
by A9, Th1;
hence
ex
L being
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) st
{A,B} on L
;
verum end;
now ( a <> b implies ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L )assume
a <> b
;
ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on Lthen
{a,b} in Li
;
then consider l being
Element of
Li such that A10:
l = {a,b}
;
reconsider L =
l as
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
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
ex
L being
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) st
{A,B} on L
;
verum end;
hence
ex
L being
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) st
{A,B} on L
by A5;
verum
end; A12:
for
a being
Element of
{0,1,2,3} for
l being
Element of
Li st
[a,l] in i1 holds
a in l
proof
let a be
Element of
{0,1,2,3};
for l being Element of Li st [a,l] in i1 holds
a in llet l be
Element of
Li;
( [a,l] in i1 implies a in l )
assume
[a,l] in i1
;
a in l
then consider b being
Element of
{0,1,2,3},
k being
Element of
Li such that A13:
[a,l] = [b,k]
and A14:
b in k
;
a = b
by A13, XTUPLE_0:1;
hence
a in l
by A13, A14, XTUPLE_0:1;
verum
end; thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
up-2-rank
( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_non-empty_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is planar & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_<=1_plane_per_3_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )proof
let A,
B be
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 10 for K, L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st A <> B & {A,B} on K & {A,B} on L holds
K = Llet K,
L be
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
( A <> B & {A,B} on K & {A,B} on L implies K = L )
assume that A15:
A <> B
and A16:
{A,B} on K
and A17:
{A,B} on L
;
K = 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 being
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 being
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
K = L
by A15, A22, A18, A19, A20, A21, TARSKI:def 2;
verum
end; thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
with_non-empty_planes
( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is planar & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_<=1_plane_per_3_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )proof
let P be
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 11 ex A being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st A on P
reconsider p =
P as
Element of
Pl ;
p in Pl
;
then consider a,
b,
c being
Element of
{0,1,2,3} such that A23:
p = {a,b,c}
and
a <> b
and
a <> c
and
b <> c
;
reconsider A =
a as
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
take
A
;
A on P
a in p
by A23, ENUMSET1:def 1;
then
[a,p] in i2
;
hence
A on P
;
verum
end; thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
planar
( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_<=1_plane_per_3_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )proof
let A,
B,
C be
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 12 ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P
reconsider a =
A,
b =
B,
c =
C as
Element of
{0,1,2,3} ;
A24:
now ( a = b & a = c & b = c implies ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P )
for
a being
Element of
{0,1,2,3} ex
b,
c being
Element of
{0,1,2,3} st
(
a <> b &
a <> c &
b <> c )
proof
let a be
Element of
{0,1,2,3};
ex b, c being Element of {0,1,2,3} st
( a <> b & a <> c & b <> c )
A25:
now ( ( a = 2 or a = 3 ) implies ex b, c being Element of {0,1,2,3} st
( a <> b & a <> c & b <> c ) )assume
(
a = 2 or
a = 3 )
;
ex b, c being Element of {0,1,2,3} st
( a <> b & a <> c & b <> c )then
(
a <> Zero1 &
a <> One )
;
hence
ex
b,
c being
Element of
{0,1,2,3} st
(
a <> b &
a <> c &
b <> c )
;
verum end;
now ( ( a = 0 or a = 1 ) implies ex b, c being Element of {0,1,2,3} st
( a <> b & a <> c & b <> c ) )assume
(
a = 0 or
a = 1 )
;
ex b, c being Element of {0,1,2,3} st
( a <> b & a <> c & b <> c )then
(
a <> Two &
a <> Three )
;
hence
ex
b,
c being
Element of
{0,1,2,3} st
(
a <> b &
a <> c &
b <> c )
;
verum end;
hence
ex
b,
c being
Element of
{0,1,2,3} st
(
a <> b &
a <> c &
b <> c )
by A25, ENUMSET1:def 2;
verum
end; then consider x,
y being
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 being
Element of
Pl such that A27:
p = {a,x,y}
;
reconsider P =
p as
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
assume that A28:
(
a = b &
a = c )
and
b = c
;
ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P
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
ex
P being
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) st
{A,B,C} on P
;
verum end;
A29:
now ( ( ( a = b & a <> c ) or ( a = c & a <> b ) or ( b = c & a <> b ) ) implies ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P )assume A30:
( (
a = b &
a <> c ) or (
a = c &
a <> b ) or (
b = c &
a <> b ) )
;
ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on Pthen consider x,
y being
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 being
Element of
{0,1,2,3} ex
c being
Element of
{0,1,2,3} st
(
a <> c &
b <> c )
proof
let a,
b be
Element of
{0,1,2,3};
ex c being Element of {0,1,2,3} st
( a <> c & b <> c )
A36:
now ( ( a = 1 or a = 2 or a = 3 ) & ( b = 1 or b = 2 or b = 3 ) implies ex c being Element of {0,1,2,3} st
( a <> c & b <> c ) )assume that A37:
(
a = 1 or
a = 2 or
a = 3 )
and A38:
(
b = 1 or
b = 2 or
b = 3 )
;
ex c being Element of {0,1,2,3} st
( a <> c & b <> c )
a <> Zero1
by A37;
hence
ex
c being
Element of
{0,1,2,3} st
(
a <> c &
b <> c )
by A38;
verum end;
A42:
now ( ( a = 1 or a = 2 ) & b = 0 implies ex c being Element of {0,1,2,3} st
( a <> c & b <> c ) )assume that A43:
(
a = 1 or
a = 2 )
and A44:
b = 0
;
ex c being Element of {0,1,2,3} st
( a <> c & b <> c )
a <> Three
by A43;
hence
ex
c being
Element of
{0,1,2,3} st
(
a <> c &
b <> c )
by A44;
verum end;
hence
ex
c being
Element of
{0,1,2,3} st
(
a <> c &
b <> c )
by A33, A36, A42, A39, ENUMSET1:def 2;
verum
end; then consider z being
Element of
{0,1,2,3} such that A47:
(
x <> z &
y <> z )
;
{x,y,z} in Pl
by A32, A47;
then consider p being
Element of
Pl such that A48:
p = {x,y,z}
;
reconsider P =
p as
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
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
ex
P being
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) st
{A,B,C} on P
;
verum end;
now ( a <> b & a <> c & b <> c implies ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P )assume
(
a <> b &
a <> c &
b <> c )
;
ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on Pthen
{a,b,c} in Pl
;
then consider p being
Element of
Pl such that A51:
p = {a,b,c}
;
reconsider P =
p as
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
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
ex
P being
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) st
{A,B,C} on P
;
verum end;
hence
ex
P being
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) st
{A,B,C} on P
by A24, A29;
verum
end; A54:
for
a being
Element of
{0,1,2,3} for
p being
Element of
Pl st
[a,p] in i2 holds
a in p
proof
let a be
Element of
{0,1,2,3};
for p being Element of Pl st [a,p] in i2 holds
a in plet p be
Element of
Pl;
( [a,p] in i2 implies a in p )
assume
[a,p] in i2
;
a in p
then consider b being
Element of
{0,1,2,3},
q being
Element of
Pl such that A55:
[a,p] = [b,q]
and A56:
b in q
;
a = b
by A55, XTUPLE_0:1;
hence
a in p
by A55, A56, XTUPLE_0:1;
verum
end; thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
with_<=1_plane_per_3_pts
( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )proof
let A,
B,
C be
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 13 for P, Q being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Qlet P,
Q be
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
( not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q implies P = Q )
assume that A57:
not
{A,B,C} is
linear
and A58:
{A,B,C} on P
and A59:
{A,B,C} on Q
;
P = 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 being
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 being
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 ( not A = B & not A = C & not B = C )consider L being
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #)
such that A67:
{A,C} on L
by A4;
A68:
(
A on L &
C on L )
by A67, Th1;
consider K being
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #)
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 )
;
contradiction
(
A on K &
B on K )
by A69, Th1;
hence
contradiction
by A71, A68, A70, Th2;
verum 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
P = Q
by A66, A60, A61, A63, A62, A64, A65, A72, ENUMSET1:57, ENUMSET1:58, ENUMSET1:59, ENUMSET1:60;
verum
end; thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
with_lines_inside_planes
( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )proof
let L be
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 14 for P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st ex A, B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on Plet P be
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
( ex A, B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st
( A <> B & {A,B} on L & {A,B} on P ) implies L on P )
given A,
B being
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #)
such that A73:
A <> B
and A74:
{A,B} on L
and A75:
{A,B} on P
;
L 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 for x being object st x in l holds
x in plet x be
object ;
( x in l implies x in p )assume A80:
x in l
;
x in p
l in Li
;
then consider x1,
x2 being
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;
verum end;
then
l c= p
;
then
[l,p] in i3
;
hence
L on P
;
verum
end; thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
with_planes_intersecting_in_2_pts
( IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional & IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible )proof
let A be
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 15 for P, Q being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st A on P & A on Q holds
ex B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st
( A <> B & B on P & B on Q )let P,
Q be
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
( A on P & A on Q implies ex B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st
( A <> B & B on P & B on Q ) )
assume that A83:
A on P
and A84:
A on Q
;
ex B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st
( A <> B & B on P & B 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 being
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 being
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 being
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 being
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 ( z1 <> z3 & z1 <> z4 & z2 <> z3 implies not z2 <> z4 )assume A100:
(
z1 <> z3 &
z1 <> z4 &
z2 <> z3 &
z2 <> z4 )
;
contradictionper cases
( a = 0 or a = 1 or a = 2 or a = 3 )
by ENUMSET1:def 2;
suppose A101:
a = 0
;
contradictionthen 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;
verum end; suppose A104:
a = 1
;
contradictionthen 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;
verum end; suppose A107:
a = 2
;
contradictionthen 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;
verum end; suppose A110:
a = 3
;
contradictionthen 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;
verum end; end; end;
then consider z being
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
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
take
B
;
( A <> B & B on P & B on Q )
thus
A <> B
by A114;
( B on P & B on Q )
(
[z,p] in i2 &
[z,q] in i2 )
by A113;
hence
(
B on P &
B on Q )
;
verum
end; thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
up-3-dimensional
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible 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
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) ;
take
A
;
INCSP_1:def 16 not for B, C, D being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) holds {A,B,C,D} is planar
take
B
;
not for C, D being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) holds {A,B,C,D} is planar
take
C
;
not for D being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) holds {A,B,C,D} is planar
take
D
;
not {A,B,C,D} is planar
assume
{A,B,C,D} is
planar
;
contradiction
then consider P being
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #)
such that A115:
{A,B,C,D} on P
;
reconsider p =
P as
Element of
Pl ;
p in Pl
;
then consider a,
b,
c being
Element of
{0,1,2,3} 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;
verum
end; A120:
for
p being
Element of
Pl for
l being
Element of
Li st
[l,p] in i3 holds
l c= p
thus
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #) is
inc-compatible
verumproof
let A be
POINT of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
INCSP_1:def 17 for L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #)
for P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st A on L & L on P holds
A on Plet L be
LINE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
for P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st A on L & L on P holds
A on Plet P be
PLANE of
IncStruct(#
{0,1,2,3},
Li,
Pl,
i1,
i2,
i3 #);
( A on L & L on P implies A on P )
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
;
A 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
A on P
;
verum
end; end;
then
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is IncSpace-like
;
hence
ex b1 being IncStruct st
( b1 is strict & b1 is IncSpace-like )
; verum