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 ; :: 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;
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 ; :: 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;
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:]
proof
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;
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 :: 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 )
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 )
proof
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 ;
then [b,l] in i1 ;
then A3: B on L ;
a in l by ;
then [a,l] in i1 ;
then A on L ;
hence {A,B} on L by ; :: thesis: verum
end;
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 )
proof
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} ;
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
proof
let a be Element of {0,1,2,3}; :: thesis: ex c being Element of {0,1,2,3} st a <> c
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;
now :: thesis: ( a = 0 implies ex c being Element of {0,1,2,3} st a <> c )
assume 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;
hence ex c being Element of {0,1,2,3} st a <> c by ; :: thesis: 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 ;
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 ;
hence ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L ; :: thesis: verum
end;
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 )
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} 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 ;
then [b,l] in i1 ;
then A11: B on L ;
a in l by ;
then [a,l] in i1 ;
then A on L ;
then {A,B} on L by ;
hence ex L being LINE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B} on L ; :: thesis: 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; :: thesis: 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}; :: 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 ;
hence a in l by ; :: thesis: verum
end;
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 )
proof
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 ;
then [b,k] in i1 ;
then b in k by A12;
then A19: ( b = x1 or b = x2 ) by ;
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 ;
then [a,l] in i1 ;
then a in l by A12;
then A21: ( a = x3 or a = x4 ) by ;
B on L by ;
then [b,l] in i1 ;
then A22: b in l by A12;
A on K by ;
then [a,k] in i1 ;
then a in k by A12;
then ( a = x1 or a = x2 ) by ;
hence K = L by ; :: thesis: verum
end;
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 )
proof
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 ;
then [a,p] in i2 ;
hence A on P ; :: thesis: verum
end;
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 )
proof
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} ;
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 )
proof
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 )

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 ) )
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;
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 ) )
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;
hence ex b, c being Element of {0,1,2,3} st
( a <> b & a <> c & b <> c ) by ; :: thesis: 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 ; :: 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 ;
then [a,p] in i2 ;
then A on P ;
then {A,B,C} on P by ;
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;
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 )
proof
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 )

A33: now :: thesis: ( a = 0 & b = 3 implies ex c being Element of {0,1,2,3} st
( 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;
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 ) )
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;
A39: now :: thesis: ( a = 3 & b = 0 implies ex c being Element of {0,1,2,3} st
( 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;
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 ) )
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;
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 ) )
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;
hence ex c being Element of {0,1,2,3} st
( a <> c & b <> c ) by ; :: thesis: 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 ;
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 ;
then [b,p] in i2 ;
then A49: B on P ;
c in p by ;
then [c,p] in i2 ;
then A50: C on P ;
a in p by ;
then [a,p] in i2 ;
then A on P ;
then {A,B,C} on P by ;
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;
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 )
assume ( 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 ;
then [b,p] in i2 ;
then A52: B on P ;
c in p by ;
then [c,p] in i2 ;
then A53: C on P ;
a in p by ;
then [a,p] in i2 ;
then A on P ;
then {A,B,C} on P by ;
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;
hence ex P being PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) st {A,B,C} on P by ; :: thesis: 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}; :: 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 ;
hence a in p by ; :: thesis: verum
end;
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 )
proof
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 ;
then [a,p] in i2 ;
then a in p by A54;
then A61: ( a = x1 or a = x2 or a = x3 ) by ;
C on P by ;
then [c,p] in i2 ;
then c in p by A54;
then A62: ( c = x1 or c = x2 or c = x3 ) by ;
B on P by ;
then [b,p] in i2 ;
then b in p by A54;
then A63: ( b = x1 or b = x2 or b = x3 ) by ;
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 ;
then [b,q] in i2 ;
then b in q by A54;
then A65: ( b = x1 or b = x2 or b = x3 ) by ;
A66: now :: thesis: ( 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 ;
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 ;
hence contradiction by A71, A68, A70, Th2; :: thesis: verum
end;
C on Q by ;
then [c,q] in i2 ;
then c in q by A54;
then A72: ( c = x1 or c = x2 or c = x3 ) by ;
A on Q by ;
then [a,q] in i2 ;
then a in q by A54;
then ( a = x1 or a = x2 or a = x3 ) by ;
hence P = Q by ; :: thesis: verum
end;
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 )
proof
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 ;
then [a,p] in i2 ;
then A76: a in p by A54;
reconsider l = L as Element of Li ;
B on L by ;
then [b,l] in i1 ;
then A77: b in l by A12;
B on P by ;
then [b,p] in i2 ;
then A78: b in p by A54;
A on L by ;
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
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 ;
( a = x1 or a = x2 ) by ;
hence x in p by ; :: thesis: verum
end;
then l c= p ;
then [l,p] in i3 ;
hence L on P ; :: thesis: verum
end;
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 )
proof
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 ;
A88: x3 in p by ;
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 ;
A92: y3 in q by ;
[a,q] in i2 by A84;
then a in q by A54;
then ( a = y1 or a = y2 or a = y3 ) by ;
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 ;
[a,p] in i2 by A83;
then a in p by A54;
then ( a = x1 or a = x2 or a = x3 ) by ;
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 ;
now :: thesis: ( z1 <> z3 & z1 <> z4 & z2 <> z3 implies not z2 <> z4 )
assume A100: ( z1 <> z3 & z1 <> z4 & z2 <> z3 & z2 <> z4 ) ; :: thesis: contradiction
per cases ( a = 0 or a = 1 or a = 2 or a = 3 ) by ENUMSET1:def 2;
suppose A101: a = 0 ; :: thesis: contradiction
then A102: ( z3 = 1 or z3 = 2 or z3 = 3 ) by ;
A103: ( z2 = 1 or z2 = 2 or z2 = 3 ) by ;
( z1 = 1 or z1 = 2 or z1 = 3 ) by ;
hence contradiction by A99, A95, A100, A101, A103, A102, ENUMSET1:def 2; :: thesis: verum
end;
suppose A104: a = 1 ; :: thesis: contradiction
then A105: ( z3 = 0 or z3 = 2 or z3 = 3 ) by ;
A106: ( z2 = 0 or z2 = 2 or z2 = 3 ) by ;
( z1 = 0 or z1 = 2 or z1 = 3 ) by ;
hence contradiction by A99, A95, A100, A104, A106, A105, ENUMSET1:def 2; :: thesis: verum
end;
suppose A107: a = 2 ; :: thesis: contradiction
then A108: ( z3 = 0 or z3 = 1 or z3 = 3 ) by ;
A109: ( z2 = 0 or z2 = 1 or z2 = 3 ) by ;
( z1 = 0 or z1 = 1 or z1 = 3 ) by ;
hence contradiction by A99, A95, A100, A107, A109, A108, ENUMSET1:def 2; :: thesis: verum
end;
suppose A110: a = 3 ; :: thesis: contradiction
then A111: ( z3 = 0 or z3 = 1 or z3 = 2 ) by ;
A112: ( z2 = 0 or z2 = 1 or z2 = 2 ) by ;
( z1 = 0 or z1 = 1 or z1 = 2 ) by ;
hence contradiction by A99, A95, A100, A110, A112, A111, ENUMSET1:def 2; :: thesis: 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 ; :: 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;
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
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 ; :: 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 ;
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 ;
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 ;
hence contradiction by A116, A117, A119, A118, ENUMSET1:def 1; :: thesis: verum
end;
A120: for p being Element of Pl
for l being Element of Li st [l,p] in i3 holds
l c= p
proof
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 ;
hence l c= p by ; :: thesis: verum
end;
thus IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is inc-compatible :: 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;
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 ) ; :: thesis: verum