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 ;

now

set S = IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #);
A1: 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
A2: [a,l] = [b,k] and
A3: b in k ;
( a = b & l = k ) by A2, ZFMISC_1:33;
hence a in l by A3; :: thesis:

end;

A4: 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
A5: [a,p] = [b,q] and
A6: b in q ;
( a = b & p = q ) by A5, ZFMISC_1:33;
hence a in p by A6; :: thesis:

end;

A7: 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
A8: [l,p] = [k,q] and
A9: k c= q ;
( l = k & p = q ) by A8, ZFMISC_1:33;
hence l c= p by A9; :: thesis:

end;

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
A10: l = {a,b} and
A11: 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 A11; :: thesis:
( a in l & b in l ) by A10, TARSKI:def 2;
then ( [a,l] in i1 & [b,l] in i1 ) ;
then ( A on L & B on L ) by Def1;
hence {A,B} on L by Th11; :: thesis:

end;

thus A12: 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} ;

A13: now

assume a <> b ; :: thesis:
then {a,b} in Li ;
then consider l being Element of Li such that
A14: l = {a,b} ;
reconsider L = l as LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) ;
( a in l & b in l ) by A14, TARSKI:def 2;
then ( [a,l] in i1 & [b,l] in i1 ) ;
then ( A on L & B on L ) by Def1;
then {A,B} on L by Th11;
hence ex L being LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L ; :: thesis:

end;

now

assume A15: a = b ; :: thesis:
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:

A16: now

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

end;

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;

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

end;

then consider c being Element of {0 ,1,2,3} such that
A17: a <> c ;
{a,c} in Li by A17;
then consider l being Element of Li such that
A18: l = {a,c} ;
reconsider L = l as LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) ;
a in l by A18, TARSKI:def 2;
then [a,l] in i1 ;
then ( A on L & B on L ) by A15, Def1;
then {A,B} on L by 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 A13; :: 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
A19: A <> B and
A20: {A,B} on K and
A21: {A,B} on L ; :: thesis:
reconsider k = K, l = L as Element of Li ;
A22: ( A on K & B on K ) by A20, Th11;
A23: ( A on L & B on L ) by A21, Th11;
reconsider a = A, b = B as Element of {0 ,1,2,3} ;
( [a,k] in i1 & [b,k] in i1 ) by A22, Def1;
then A24: ( a in k & b in k ) by A1;
( [a,l] in i1 & [b,l] in i1 ) by A23, Def1;
then A25: ( a in l & b in l ) by A1;
k in Li ;
then consider x1, x2 being Element of {0 ,1,2,3} such that
A26: k = {x1,x2} and
x1 <> x2 ;
A27: ( ( a = x1 or a = x2 ) & ( b = x1 or b = x2 ) ) by A24, A26, TARSKI:def 2;
l in Li ;
then consider x3, x4 being Element of {0 ,1,2,3} such that
A28: l = {x3,x4} and
x3 <> x4 ;
( ( a = x3 or a = x4 ) & ( b = x3 or b = x4 ) ) by A25, A28, TARSKI:def 2;
hence K = L by A19, A26, A27, A28; :: 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
A29: p = {a,b,c} and
( a <> b & a <> c & 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 A29, 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} ;

A30: now

assume ( a <> b & a <> c & b <> c ) ; :: thesis:
then {a,b,c} in Pl ;
then consider p being Element of Pl such that
A31: p = {a,b,c} ;
reconsider P = p as PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) ;
( a in p & b in p & c in p ) by A31, ENUMSET1:def 1;
then ( [a,p] in i2 & [b,p] in i2 & [c,p] in i2 ) ;
then ( A on P & B on P & C on P ) by Def2;
then {A,B,C} on P by 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;

A32: now

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

A34: now

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

end;

now

assume ( a = 2 or a = 3 ) ; :: thesis:
then ( a <> Zero1 & a <> One & Zero1 <> One ) ;
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 A34, ENUMSET1:def 2; :: thesis:

end;

then consider x, y being Element of {0 ,1,2,3} such that
A35: ( a <> x & a <> y & x <> y ) ;
{a,x,y} in Pl by A35;
then consider p being Element of Pl such that
A36: p = {a,x,y} ;
reconsider P = p as PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) ;
a in p by A36, ENUMSET1:def 1;
then [a,p] in i2 ;
then A on P by Def2;
then {A,B,C} on P by A33, 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;

now

assume A37: ( ( 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
A38: ( ( x = a or x = b or x = c ) & ( y = a or y = b or y = c ) ) and
A39: 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:

A40: now

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

end;

A41: now

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

end;

A42: now

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

end;

A43: now

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

end;

now

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

end;

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

end;

then consider z being Element of {0 ,1,2,3} such that
A44: ( x <> z & y <> z ) ;
{x,y,z} in Pl by A39, A44;
then consider p being Element of Pl such that
A45: p = {x,y,z} ;
reconsider P = p as PLANE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) ;
( a in p & b in p & c in p ) by A37, A38, A39, A45, ENUMSET1:def 1;
then ( [a,p] in i2 & [b,p] in i2 & [c,p] in i2 ) ;
then ( A on P & B on P & C on P ) by Def2;
then {A,B,C} on P by 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 A30, A32; :: 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
A46: not {A,B,C} is linear and
A47: {A,B,C} on P and
A48: {A,B,C} on Q ; :: thesis:
reconsider p = P, q = Q as Element of Pl ;

A49: now

assume A50: ( A = B or A = C or B = C ) ; :: thesis:
consider K being LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) such that
A51: {A,B} on K by A12, Def9;
consider L being LINE of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) such that
A52: {A,C} on L by A12, Def9;
A53: ( A on K & B on K & A on L & C on L ) by A51, A52, Th11;
( not {A,B,C} on K & not {A,B,C} on L ) by A46, Def6;
hence contradiction by A50, A53, Th12; :: thesis:

end;

A54: ( A on P & B on P & C on P ) by A47, Th14;
reconsider a = A, b = B, c = C as Element of {0 ,1,2,3} ;
( [a,p] in i2 & [b,p] in i2 & [c,p] in i2 ) by A54, Def2;
then A55: ( a in p & b in p & c in p ) by A4;
p in Pl ;
then consider x1, x2, x3 being Element of {0 ,1,2,3} such that
A56: p = {x1,x2,x3} and
( x1 <> x2 & x1 <> x3 & x2 <> x3 ) ;
A57: ( ( a = x1 or a = x2 or a = x3 ) & ( b = x1 or b = x2 or b = x3 ) & ( c = x1 or c = x2 or c = x3 ) ) by A55, A56, ENUMSET1:def 1;
( A on Q & B on Q & C on Q ) by A48, Th14;
then ( [a,q] in i2 & [b,q] in i2 & [c,q] in i2 ) by Def2;
then A58: ( a in q & b in q & c in q ) by A4;
q in Pl ;
then consider x1, x2, x3 being Element of {0 ,1,2,3} such that
A59: q = {x1,x2,x3} and
( x1 <> x2 & x1 <> x3 & x2 <> x3 ) ;
( ( a = x1 or a = x2 or a = x3 ) & ( b = x1 or b = x2 or b = x3 ) & ( c = x1 or c = x2 or c = x3 ) ) by A58, A59, ENUMSET1:def 1;
hence P = Q by A49, A56, A57, A59, 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 A60: A <> B and
A61: {A,B} on L and
A62: {A,B} on P ; :: thesis:
reconsider l = L as Element of Li ;
reconsider p = P as Element of Pl ;
reconsider a = A, b = B as Element of {0 ,1,2,3} ;
( A on L & B on L ) by A61, Th11;
then ( [a,l] in i1 & [b,l] in i1 ) by Def1;
then A63: ( a in l & b in l ) by A1;
( A on P & B on P ) by A62, Th13;
then ( [a,p] in i2 & [b,p] in i2 ) by Def2;
then A64: ( a in p & b in p ) by A4;

now

let x be set ; :: thesis:
assume A65: x in l ; :: thesis:
l in Li ;
then consider x1, x2 being Element of {0 ,1,2,3} such that
A66: l = {x1,x2} and
x1 <> x2 ;
( ( a = x1 or a = x2 ) & ( b = x1 or b = x2 ) ) by A63, A66, TARSKI:def 2;
hence x in p by A60, A64, A65, A66, 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
A67: A on P and
A68: A on Q ; :: thesis:
reconsider a = A 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
A69: p = {x1,x2,x3} and
A70: ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) ;
q in Pl ;
then consider y1, y2, y3 being Element of {0 ,1,2,3} such that
A71: q = {y1,y2,y3} and
A72: ( y1 <> y2 & y1 <> y3 & y2 <> y3 ) ;
A73: ( x1 in p & x2 in p & x3 in p ) by A69, ENUMSET1:def 1;
A74: ( y1 in q & y2 in q & y3 in q ) by A71, ENUMSET1:def 1;
[a,p] in i2 by A67, Def2;
then a in p by A4;
then ( a = x1 or a = x2 or a = x3 ) by A69, ENUMSET1:def 1;
then consider z1, z2 being Element of {0 ,1,2,3} such that
A75: ( z1 in p & z2 in p ) and
A76: ( z1 <> a & z2 <> a ) and
A77: z1 <> z2 by A70, A73;
[a,q] in i2 by A68, Def2;
then a in q by A4;
then ( a = y1 or a = y2 or a = y3 ) by A71, ENUMSET1:def 1;
then consider z3, z4 being Element of {0 ,1,2,3} such that
A78: ( z3 in q & z4 in q ) and
A79: ( z3 <> a & z4 <> a ) and
A80: z3 <> z4 by A72, A74;

now

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

per cases by ENUMSET1:def 2;

suppose A82: a = 0 ; :: thesis:

then A83: ( ( z1 = 1 or z1 = 2 or z1 = 3 ) & ( z2 = 1 or z2 = 2 or z2 = 3 ) ) by A76, ENUMSET1:def 2;
( ( z3 = 1 or z3 = 2 or z3 = 3 ) & ( z4 = 1 or z4 = 2 or z4 = 3 ) ) by A79, A82, ENUMSET1:def 2;
hence contradiction by A77, A80, A81, A83; :: thesis:

end;

suppose A84: a = 1 ; :: thesis:

then A85: ( ( z1 = 0 or z1 = 2 or z1 = 3 ) & ( z2 = 0 or z2 = 2 or z2 = 3 ) ) by A76, ENUMSET1:def 2;
( ( z3 = 0 or z3 = 2 or z3 = 3 ) & ( z4 = 0 or z4 = 2 or z4 = 3 ) ) by A79, A84, ENUMSET1:def 2;
hence contradiction by A77, A80, A81, A85; :: thesis:

end;

suppose A86: a = 2 ; :: thesis:

then A87: ( ( z1 = 0 or z1 = 1 or z1 = 3 ) & ( z2 = 0 or z2 = 1 or z2 = 3 ) ) by A76, ENUMSET1:def 2;
( ( z3 = 0 or z3 = 1 or z3 = 3 ) & ( z4 = 0 or z4 = 1 or z4 = 3 ) ) by A79, A86, ENUMSET1:def 2;
hence contradiction by A77, A80, A81, A87; :: thesis:

end;

suppose A88: a = 3 ; :: thesis:

then A89: ( ( z1 = 0 or z1 = 1 or z1 = 2 ) & ( z2 = 0 or z2 = 1 or z2 = 2 ) ) by A76, ENUMSET1:def 2;
( ( z3 = 0 or z3 = 1 or z3 = 2 ) & ( z4 = 0 or z4 = 1 or z4 = 2 ) ) by A79, A88, ENUMSET1:def 2;
hence contradiction by A77, A80, A81, A89; :: thesis:

end;

end;

end;

then consider z being Element of {0 ,1,2,3} such that
A90: ( z in p & z in q ) and
A91: a <> z by A75, A76, A78;
reconsider B = z as POINT of IncStruct(# {0 ,1,2,3},Li,Pl,i1,i2,i3 #) ;
take B ; :: thesis:
thus A <> B by A91; :: thesis:
( [z,p] in i2 & [z,q] in i2 ) by A90;
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
A92: {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
A93: p = {a,b,c} and
( a <> b & a <> c & b <> c ) ;
( A on P & B on P & C on P & D on P ) by A92, Th15;
then ( [Zero1,p] in i2 & [One,p] in i2 & [Two,p] in i2 & [Three,p] in i2 ) by Def2;
then ( Zero1 in p & One in p & Two in p & Three in p ) by A4;
then ( ( Zero1 = a or Zero1 = b or Zero1 = c ) & ( One = a or One = b or One = c ) & ( Two = a or Two = b or Two = c ) & ( Three = a or Three = b or Three = c ) ) by A93, ENUMSET1:def 1;
hence contradiction ; :: 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 ( A on L & L on P ) ; :: thesis:
then ( [a,l] in i1 & [l,p] in i3 ) by Def1, Def3;
then ( a in l & l c= p ) by A1, A7;
then [a,p] in i2 ;
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: