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

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

{ [l,p] where l is Element of Li, p is Element of Pl : l c= p } c= [:Li,Pl:]

hence ex b_{1} being IncStruct st

( b_{1} is strict & b_{1} is IncSpace-like )
; :: thesis: verum

{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

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 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 } ; :: thesis: 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:] ; :: thesis: verum

end;assume x in { [a,l] where a is Element of {0,1,2,3}, l is Element of Li : a in l } ; :: thesis: 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:] ; :: thesis: verum

{ [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

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 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 } ; :: thesis: 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:] ; :: thesis: verum

end;assume x in { [a,p] where a is Element of {0,1,2,3}, p is Element of Pl : a in p } ; :: thesis: 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:] ; :: thesis: verum

{ [l,p] where l is Element of Li, p is Element of Pl : l c= p } c= [:Li,Pl:]

proof

then reconsider i3 = { [l,p] where l is Element of Li, p is Element of Pl : l c= p } as Relation of Li,Pl ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [l,p] where l is Element of Li, p is Element of Pl : l c= p } or x in [:Li,Pl:] )

assume x in { [l,p] where l is Element of Li, p is Element of Pl : l c= p } ; :: thesis: x in [:Li,Pl:]

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

end;assume x in { [l,p] where l is Element of Li, p is Element of Pl : l c= p } ; :: thesis: x in [:Li,Pl:]

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

now :: thesis: ( 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 )

then
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is IncSpace-like
;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: ( 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 )

for l being Element of Li st [a,l] in i1 holds

a in l

for p being Element of Pl st [a,p] in i2 holds

a in p

for l being Element of Li st [l,p] in i3 holds

l c= p

end;thus IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_non-trivial_lines :: thesis: ( 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

thus A4:
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is linear
:: thesis: ( 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 )
let L be LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 8 :: thesis: 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 ; :: thesis: ex B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st

( A <> B & {A,B} on L )

take B ; :: thesis: ( A <> B & {A,B} on L )

thus A <> B by A2; :: thesis: {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; :: thesis: verum

end;( 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 ; :: thesis: ex B being POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st

( A <> B & {A,B} on L )

take B ; :: thesis: ( A <> B & {A,B} on L )

thus A <> B by A2; :: thesis: {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; :: thesis: verum

proof

A12:
for a being Element of {0,1,2,3}
let A, B be POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 9 :: thesis: 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} ;

end;reconsider a = A, b = B as Element of {0,1,2,3} ;

A5: now :: thesis: ( 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

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 ; :: thesis: ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L

then {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 ; :: thesis: verum

end;proof

then consider c being Element of {0,1,2,3} such that
let a be Element of {0,1,2,3}; :: thesis: ex c being Element of {0,1,2,3} st a <> c

end;A6: now :: thesis: ( ( 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 )
; :: thesis: ex c being Element of {0,1,2,3} st a <> c

then a <> Zero1 ;

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

end;then a <> Zero1 ;

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

now :: thesis: ( a = 0 implies ex c being Element of {0,1,2,3} st a <> c )

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

then a <> One ;

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

end;then a <> One ;

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

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 ; :: thesis: ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L

then {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 ; :: thesis: verum

now :: thesis: ( a <> b implies ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L )

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

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 ;

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

end;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 ;

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

for l being Element of Li st [a,l] in i1 holds

a in l

proof

thus
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-2-rank
:: thesis: ( 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 )
let a be Element of {0,1,2,3}; :: thesis: for l being Element of Li st [a,l] in i1 holds

a in l

let l be Element of Li; :: thesis: ( [a,l] in i1 implies a in l )

assume [a,l] in i1 ; :: thesis: 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; :: thesis: verum

end;a in l

let l be Element of Li; :: thesis: ( [a,l] in i1 implies a in l )

assume [a,l] in i1 ; :: thesis: 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; :: thesis: verum

proof

thus
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_non-empty_planes
:: thesis: ( 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 )
let A, B be POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 10 :: thesis: 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 = L

let K, L be LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;K = L

let K, L be LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

proof

thus
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is planar
:: thesis: ( 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 )
let P be PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 11 :: thesis: 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 ; :: thesis: A on P

a in p by A23, ENUMSET1:def 1;

then [a,p] in i2 ;

hence A on P ; :: thesis: verum

end;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 on P

a in p by A23, ENUMSET1:def 1;

then [a,p] in i2 ;

hence A on P ; :: thesis: verum

proof

A54:
for a being Element of {0,1,2,3}
let A, B, C be POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 12 :: thesis: 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} ;

end;reconsider a = A, b = B, c = C as Element of {0,1,2,3} ;

A24: now :: thesis: ( 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 )

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

end;( a <> b & a <> c & b <> c )

proof

then consider x, y being Element of {0,1,2,3} such that
let a be Element of {0,1,2,3}; :: thesis: ex b, c being Element of {0,1,2,3} st

( a <> b & a <> c & b <> c )

( a <> b & a <> c & b <> c ) by A25, ENUMSET1:def 2; :: thesis: verum

end;( a <> b & a <> c & b <> c )

A25: now :: thesis: ( ( a = 2 or a = 3 ) implies ex b, c being Element of {0,1,2,3} st

( a <> b & a <> c & b <> c ) )

( a <> b & a <> c & b <> c ) )

assume
( a = 2 or a = 3 )
; :: thesis: 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 ) ; :: thesis: verum

end;( 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 ) ; :: thesis: verum

now :: thesis: ( ( a = 0 or a = 1 ) implies ex b, c being Element of {0,1,2,3} st

( a <> b & a <> c & b <> c ) )

hence
ex b, c being Element of {0,1,2,3} st ( a <> b & a <> c & b <> c ) )

assume
( a = 0 or a = 1 )
; :: thesis: 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 ) ; :: thesis: verum

end;( 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 ) ; :: thesis: verum

( a <> b & a <> c & b <> c ) by A25, ENUMSET1:def 2; :: thesis: verum

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

A29: now :: thesis: ( ( ( 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 ) )
; :: thesis: ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P

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 )

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

end;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 )

proof

then consider z being Element of {0,1,2,3} such that
let a, b be Element of {0,1,2,3}; :: thesis: ex c being Element of {0,1,2,3} st

( a <> c & b <> c )

( a <> c & b <> c ) by A33, A36, A42, A39, ENUMSET1:def 2; :: thesis: verum

end;( a <> c & b <> c )

A33: now :: thesis: ( a = 0 & b = 3 implies ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) )

( a <> c & b <> c ) )

assume that

A34: a = 0 and

A35: b = 3 ; :: thesis: ex c being Element of {0,1,2,3} st

( a <> c & b <> c )

a <> One by A34;

hence ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) by A35; :: thesis: verum

end;A34: a = 0 and

A35: b = 3 ; :: thesis: ex c being Element of {0,1,2,3} st

( a <> c & b <> c )

a <> One by A34;

hence ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) by A35; :: thesis: verum

A36: now :: thesis: ( ( 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 ) )

( 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 ) ; :: thesis: 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; :: thesis: verum

end;A37: ( a = 1 or a = 2 or a = 3 ) and

A38: ( b = 1 or b = 2 or b = 3 ) ; :: thesis: 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; :: thesis: verum

A39: now :: thesis: ( a = 3 & b = 0 implies ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) )

( a <> c & b <> c ) )

assume that

A40: a = 3 and

A41: b = 0 ; :: thesis: ex c being Element of {0,1,2,3} st

( a <> c & b <> c )

a <> Two by A40;

hence ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) by A41; :: thesis: verum

end;A40: a = 3 and

A41: b = 0 ; :: thesis: ex c being Element of {0,1,2,3} st

( a <> c & b <> c )

a <> Two by A40;

hence ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) by A41; :: thesis: verum

A42: now :: thesis: ( ( a = 1 or a = 2 ) & b = 0 implies ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) )

( a <> c & b <> c ) )

assume that

A43: ( a = 1 or a = 2 ) and

A44: b = 0 ; :: thesis: 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; :: thesis: verum

end;A43: ( a = 1 or a = 2 ) and

A44: b = 0 ; :: thesis: 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; :: thesis: verum

now :: thesis: ( a = 0 & ( b = 0 or b = 1 or b = 2 ) implies ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) )

hence
ex c being Element of {0,1,2,3} st ( a <> c & b <> c ) )

assume that

A45: a = 0 and

A46: ( b = 0 or b = 1 or b = 2 ) ; :: thesis: ex c being Element of {0,1,2,3} st

( a <> c & b <> c )

a <> Three by A45;

hence ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) by A46; :: thesis: verum

end;A45: a = 0 and

A46: ( b = 0 or b = 1 or b = 2 ) ; :: thesis: ex c being Element of {0,1,2,3} st

( a <> c & b <> c )

a <> Three by A45;

hence ex c being Element of {0,1,2,3} st

( a <> c & b <> c ) by A46; :: thesis: verum

( a <> c & b <> c ) by A33, A36, A42, A39, ENUMSET1:def 2; :: thesis: verum

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

now :: thesis: ( 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 )

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: verumassume
( a <> b & a <> c & b <> c )
; :: thesis: ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P

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 ;

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

end;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 ;

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

for p being Element of Pl st [a,p] in i2 holds

a in p

proof

thus
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_<=1_plane_per_3_pts
:: thesis: ( 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 )
let a be Element of {0,1,2,3}; :: thesis: for p being Element of Pl st [a,p] in i2 holds

a in p

let p be Element of Pl; :: thesis: ( [a,p] in i2 implies a in p )

assume [a,p] in i2 ; :: thesis: 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; :: thesis: verum

end;a in p

let p be Element of Pl; :: thesis: ( [a,p] in i2 implies a in p )

assume [a,p] in i2 ; :: thesis: 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; :: thesis: verum

proof

thus
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_lines_inside_planes
:: thesis: ( 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 )
let A, B, C be POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 13 :: thesis: 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 = Q

let P, Q be PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: ( 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 ; :: thesis: 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;

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

end;P = Q

let P, Q be PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: ( 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 ; :: thesis: 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 :: thesis: ( not A = B & not A = C & not B = C )

C on Q
by A59, Th4;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 ) ; :: thesis: contradiction

( A on K & B on K ) by A69, Th1;

hence contradiction by A71, A68, A70, Th2; :: thesis: verum

end;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 ) ; :: thesis: contradiction

( A on K & B on K ) by A69, Th1;

hence contradiction by A71, A68, A70, Th2; :: thesis: verum

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

proof

thus
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is with_planes_intersecting_in_2_pts
:: thesis: ( 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 )
let L be LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 14 :: thesis: 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 P

let P be PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: ( 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 ; :: thesis: 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;

then [l,p] in i3 ;

hence L on P ; :: thesis: verum

end;( A <> B & {A,B} on L & {A,B} on P ) holds

L on P

let P be PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: ( 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 ; :: thesis: 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 :: thesis: for x being object st x in l holds

x in p

then
l c= p
;x in p

let x be object ; :: thesis: ( x in l implies x in p )

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

end;assume A80: x in l ; :: thesis: 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; :: thesis: verum

then [l,p] in i3 ;

hence L on P ; :: thesis: verum

proof

thus
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is up-3-dimensional
:: thesis: IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible
let A be POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 15 :: thesis: 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 #); :: thesis: ( 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 ; :: thesis: 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;

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: ( A <> B & B on P & B on Q )

thus A <> B by A114; :: thesis: ( B on P & B on Q )

( [z,p] in i2 & [z,q] in i2 ) by A113;

hence ( B on P & B on Q ) ; :: thesis: verum

end;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 #); :: thesis: ( 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 ; :: thesis: 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 :: thesis: ( z1 <> z3 & z1 <> z4 & z2 <> z3 implies not z2 <> z4 )

then consider z being Element of {0,1,2,3} such that assume A100:
( z1 <> z3 & z1 <> z4 & z2 <> z3 & z2 <> z4 )
; :: thesis: contradiction

end;per cases
( a = 0 or a = 1 or a = 2 or a = 3 )
by ENUMSET1:def 2;

end;

suppose A101:
a = 0
; :: thesis: contradiction

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

end;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: verum

suppose A104:
a = 1
; :: thesis: contradiction

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

end;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: verum

suppose A107:
a = 2
; :: thesis: contradiction

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

end;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: verum

suppose A110:
a = 3
; :: thesis: contradiction

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

end;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: verum

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: ( A <> B & B on P & B on Q )

thus A <> B by A114; :: thesis: ( B on P & B on Q )

( [z,p] in i2 & [z,q] in i2 ) by A113;

hence ( B on P & B on Q ) ; :: thesis: verum

proof

A120:
for p being Element of Pl
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: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: not {A,B,C,D} is planar

assume {A,B,C,D} is planar ; :: thesis: 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; :: thesis: verum

end;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: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: not {A,B,C,D} is planar

assume {A,B,C,D} is planar ; :: thesis: 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; :: thesis: verum

for l being Element of Li st [l,p] in i3 holds

l c= p

proof

thus
IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible
:: thesis: verum
let p be Element of Pl; :: thesis: for l being Element of Li st [l,p] in i3 holds

l c= p

let l be Element of Li; :: thesis: ( [l,p] in i3 implies l c= p )

assume [l,p] in i3 ; :: thesis: l c= p

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, XTUPLE_0:1;

hence l c= p by A121, A122, XTUPLE_0:1; :: thesis: verum

end;l c= p

let l be Element of Li; :: thesis: ( [l,p] in i3 implies l c= p )

assume [l,p] in i3 ; :: thesis: l c= p

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, XTUPLE_0:1;

hence l c= p by A121, A122, XTUPLE_0:1; :: thesis: verum

proof

let A be POINT of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: according to INCSP_1:def 17 :: thesis: 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 P

let L be LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: 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 P

let P be PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum

end;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 P

let L be LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: 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 P

let P be PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum

hence ex b

( b