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:]

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { [a,l] where a is Element of {0 ,1,2,3}, l is Element of Li : a in l } ; :: thesis:
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:] ; :: thesis:

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:]

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { [a,p] where a is Element of {0 ,1,2,3}, p is Element of Pl : a in p } ; :: thesis:
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:] ; :: thesis:

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:]

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { [l,p] where l is Element of Li, p is Element of Pl : l c= p } ; :: thesis:
then ex l being Element of Li ex p being Element of Pl st
( x = [l,p] & l c= p ) ;
hence x in [:Li,Pl:] ; :: thesis:

end;

then reconsider i3 = { [l,p] where l is Element of Li, p is Element of Pl : l c= p } as Relation of Li,Pl ;

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 :: thesis:

let L be LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 8 :: thesis:
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 ; :: thesis:
take B ; :: thesis:
thus A <> B by A2; :: thesis:
b in l by A1, TARSKI:def 2;
then [b,l] in i1 ;
then A3: B on L by Def1;
a in l by A1, TARSKI:def 2;
then [a,l] in i1 ;
then A on L by Def1;
hence {A,B} on L by A3, Th11; :: thesis:

end;

thus A4: IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is linear :: thesis:

let A, B be POINT of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 9 :: thesis:
reconsider a = A, b = B as Element of {0 ,1,2,3} ;

A5: now

for a being Element of {0 ,1,2,3} ex c being Element of {0 ,1,2,3} st a <> c

let a be Element of {0 ,1,2,3}; :: thesis:

A6: now

assume ( a = 1 or a = 2 or a = 3 ) ; :: thesis:
then a <> Zero1 ;
hence ex c being Element of {0 ,1,2,3} st a <> c ; :: thesis:

end;

assume a = 0 ; :: thesis:
then a <> One ;
hence ex c being Element of {0 ,1,2,3} st a <> c ; :: thesis:

end;

hence ex c being Element of {0 ,1,2,3} st a <> c by A6, ENUMSET1:def 2; :: thesis:

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 by Def1;
assume a = b ; :: thesis:
then {A,B} on L by A9, Th11;
hence ex L being LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L ; :: thesis:

end;

assume a <> b ; :: thesis:
then {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 by Def1;
a in l by A10, TARSKI:def 2;
then [a,l] in i1 ;
then A on L by Def1;
then {A,B} on L by A11, Th11;
hence ex L being LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L ; :: thesis:

end;

hence ex L being LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L by A5; :: thesis:

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

let a be Element of {0 ,1,2,3}; :: thesis:
let l be Element of Li; :: thesis:
assume [a,l] in i1 ; :: thesis:
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, ZFMISC_1:33;
hence a in l by A13, A14, ZFMISC_1:33; :: thesis:

end;

thus IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is up-2-rank :: thesis:

let A, B be POINT of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 10 :: thesis:
let K, L be LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis:
assume that
A15: A <> B and
A16: {A,B} on K and
A17: {A,B} on L ; :: thesis:
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, Th11;
then [b,k] in i1 by Def1;
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, Th11;
then [a,l] in i1 by Def1;
then a in l by A12;
then A21: ( a = x3 or a = x4 ) by A20, TARSKI:def 2;
B on L by A17, Th11;
then [b,l] in i1 by Def1;
then A22: b in l by A12;
A on K by A16, Th11;
then [a,k] in i1 by Def1;
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; :: thesis:

end;

thus IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is with_non-empty_planes :: thesis:

let P be PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 11 :: thesis:
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 ; :: thesis:
a in p by A23, ENUMSET1:def 1;
then [a,p] in i2 ;
hence A on P by Def2; :: thesis:

end;

thus IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is planar :: thesis:

let A, B, C be POINT of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 12 :: thesis:
reconsider a = A, b = B, c = C as Element of {0 ,1,2,3} ;

A24: now

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 )

let a be Element of {0 ,1,2,3}; :: thesis:

A25: now

assume ( a = 2 or a = 3 ) ; :: thesis:
then ( a <> Zero1 & a <> One ) ;
hence ex b, c being Element of {0 ,1,2,3} st
( a <> b & a <> c & b <> c ) ; :: thesis:

end;

assume ( a = 0 or a = 1 ) ; :: thesis:
then ( a <> Two & a <> Three ) ;
hence ex b, c being Element of {0 ,1,2,3} st
( a <> b & a <> c & b <> c ) ; :: thesis:

end;

hence ex b, c being Element of {0 ,1,2,3} st
( a <> b & a <> c & b <> c ) by A25, ENUMSET1:def 2; :: thesis:

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 ; :: thesis:
a in p by A27, ENUMSET1:def 1;
then [a,p] in i2 ;
then A on P by Def2;
then {A,B,C} on P by A28, Th14;
hence ex P being PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P ; :: thesis:

end;

A29: now

assume A30: ( ( a = b & a <> c ) or ( a = c & a <> b ) or ( b = c & a <> b ) ) ; :: thesis:
then 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 )

let a, b be Element of {0 ,1,2,3}; :: thesis:

A33: now

assume that
A34: a = 0 and
A35: b = 3 ; :: thesis:
a <> One by A34;
hence ex c being Element of {0 ,1,2,3} st
( a <> c & b <> c ) by A35; :: thesis:

end;

A36: now

assume that
A37: ( a = 1 or a = 2 or a = 3 ) and
A38: ( b = 1 or b = 2 or b = 3 ) ; :: thesis:
a <> Zero1 by A37;
hence ex c being Element of {0 ,1,2,3} st
( a <> c & b <> c ) by A38; :: thesis:

end;

A39: now

assume that
A40: a = 3 and
A41: b = 0 ; :: thesis:
a <> Two by A40;
hence ex c being Element of {0 ,1,2,3} st
( a <> c & b <> c ) by A41; :: thesis:

end;

A42: now

assume that
A43: ( a = 1 or a = 2 ) and
A44: b = 0 ; :: thesis:
a <> Three by A43;
hence ex c being Element of {0 ,1,2,3} st
( a <> c & b <> c ) by A44; :: thesis:

end;

assume that
A45: a = 0 and
A46: ( b = 0 or b = 1 or b = 2 ) ; :: thesis:
a <> Three by A45;
hence ex c being Element of {0 ,1,2,3} st
( a <> c & b <> c ) by A46; :: thesis:

end;

hence ex c being Element of {0 ,1,2,3} st
( a <> c & b <> c ) by A33, A36, A42, A39, ENUMSET1:def 2; :: thesis:

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 by Def2;
c in p by A30, A31, A32, A48, ENUMSET1:def 1;
then [c,p] in i2 ;
then A50: C on P by Def2;
a in p by A30, A31, A32, A48, ENUMSET1:def 1;
then [a,p] in i2 ;
then A on P by Def2;
then {A,B,C} on P by A49, A50, Th14;
hence ex P being PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P ; :: thesis:

end;

assume ( a <> b & a <> c & b <> c ) ; :: thesis:
then {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 by Def2;
c in p by A51, ENUMSET1:def 1;
then [c,p] in i2 ;
then A53: C on P by Def2;
a in p by A51, ENUMSET1:def 1;
then [a,p] in i2 ;
then A on P by Def2;
then {A,B,C} on P by A52, A53, Th14;
hence ex P being PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P ; :: thesis:

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; :: thesis:

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

let a be Element of {0 ,1,2,3}; :: thesis:
let p be Element of Pl; :: thesis:
assume [a,p] in i2 ; :: thesis:
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, ZFMISC_1:33;
hence a in p by A55, A56, ZFMISC_1:33; :: thesis:

end;

thus IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is with_<=1_plane_per_3_pts :: thesis:

let A, B, C be POINT of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 13 :: thesis:
let P, Q be PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis:
assume that
A57: not {A,B,C} is linear and
A58: {A,B,C} on P and
A59: {A,B,C} on Q ; :: thesis:
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, Th14;
then [a,p] in i2 by Def2;
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, Th14;
then [c,p] in i2 by Def2;
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, Th14;
then [b,p] in i2 by Def2;
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, Th14;
then [b,q] in i2 by Def2;
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 being LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) such that
A67: {A,C} on L by A4, Def9;
A68: ( A on L & C on L ) by A67, Th11;
consider K being LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) such that
A69: {A,B} on K by A4, Def9;
A70: ( not {A,B,C} on K & not {A,B,C} on L ) by A57, Def6;
assume A71: ( A = B or A = C or B = C ) ; :: thesis:
( A on K & B on K ) by A69, Th11;
hence contradiction by A71, A68, A70, Th12; :: thesis:

end;

C on Q by A59, Th14;
then [c,q] in i2 by Def2;
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, Th14;
then [a,q] in i2 by Def2;
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:98, ENUMSET1:99, ENUMSET1:100, ENUMSET1:102; :: thesis:

end;

thus IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes :: thesis:

let L be LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 14 :: thesis:
let P be PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis:
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 ; :: thesis:
reconsider a = A, b = B as Element of {0 ,1,2,3} ;
reconsider p = P as Element of Pl ;
A on P by A75, Th13;
then [a,p] in i2 by Def2;
then A76: a in p by A54;
reconsider l = L as Element of Li ;
B on L by A74, Th11;
then [b,l] in i1 by Def1;
then A77: b in l by A12;
B on P by A75, Th13;
then [b,p] in i2 by Def2;
then A78: b in p by A54;
A on L by A74, Th11;
then [a,l] in i1 by Def1;
then A79: a in l by A12;

let x be set ; :: thesis:
assume A80: x in l ; :: thesis:
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; :: thesis:

end;

then l c= p by TARSKI:def 3;
then [l,p] in i3 ;
hence L on P by Def3; :: thesis:

end;

thus IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts :: thesis:

let A be POINT of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 15 :: thesis:
let P, Q be PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis:
assume that
A83: A on P and
A84: A on Q ; :: thesis:
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, Def2;
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, Def2;
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;

assume A100: ( z1 <> z3 & z1 <> z4 & z2 <> z3 & z2 <> z4 ) ; :: thesis:

per cases by ENUMSET1:def 2;

suppose A101: a = 0 ; :: thesis:

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; :: thesis:

end;

suppose A104: a = 1 ; :: thesis:

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; :: thesis:

end;

suppose A107: a = 2 ; :: thesis:

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; :: thesis:

end;

suppose A110: a = 3 ; :: thesis:

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; :: thesis:

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 ; :: thesis:
thus A <> B by A114; :: thesis:
( [z,p] in i2 & [z,q] in i2 ) by A113;
hence ( B on P & B on Q ) by Def2; :: thesis:

end;

thus IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional :: thesis:

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 ; :: according to INCSP_1:def 16 :: thesis:
take B ; :: thesis:
take C ; :: thesis:
take D ; :: thesis:
assume {A,B,C,D} is planar ; :: thesis:
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 by Def7;
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, Th15;
then [Three,p] in i2 by Def2;
then A117: Three in p by A54;
C on P by A115, Th15;
then [Two,p] in i2 by Def2;
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, Th15;
then [One,p] in i2 by Def2;
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, Th15;
then [Zero1,p] in i2 by Def2;
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; :: thesis:

end;

A120: for p being Element of Pl
for l being Element of Li st [l,p] in i3 holds
l c= p

let p be Element of Pl; :: thesis:
let l be Element of Li; :: thesis:
assume [l,p] in i3 ; :: thesis:
then consider k being Element of Li, q being Element of Pl such that
A121: [l,p] = [k,q] and
A122: k c= q ;
l = k by A121, ZFMISC_1:33;
hence l c= p by A121, A122, ZFMISC_1:33; :: thesis:

end;

thus IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible :: thesis:

let A be POINT of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 17 :: thesis:
let L be LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis:
let P be PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis:
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 ; :: thesis:
[l,p] in i3 by A124, Def3;
then A125: l c= p by A120;
[a,l] in i1 by A123, Def1;
then a in l by A12;
then [a,p] in i2 by A125;
hence A on P by Def2; :: thesis:

end;

end;

then IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) is IncSpace-like by Def18;
hence ex b₁ being IncStruct st
( b₁ is strict & b₁ is IncSpace-like ) ; :: thesis: