:: INCSP_1 semantic presentation

begin

definition
attrc1 is strict ;
struct IncProjStr  -> ;
aggrIncProjStr(# Points, Lines, Inc #) ->  IncProjStr ;
sel Points c1 ->  non empty set ;
sel Lines c1 ->  non empty set ;
sel Inc c1 ->  Relation of the Points of c1, the Lines of c1;
end;

definition
attrc1 is strict ;
struct IncStruct  ->  IncProjStr ;
aggrIncStruct(# Points, Lines, Planes, Inc, Inc2, Inc3 #) ->  IncStruct ;
sel Planes c1 ->  non empty set ;
sel Inc2 c1 ->  Relation of the Points of c1, the Planes of c1;
sel Inc3 c1 ->  Relation of the Lines of c1, the Planes of c1;
end;

definition
let S be IncProjStr ;
mode POINT of S is Element of the Points of S;
mode LINE of S is Element of the Lines of S;
end;

definition
let S be IncStruct ;
mode PLANE of S is Element of the Planes of S;
end;


definition
let S be IncProjStr ;
let A be POINT of S;
let L be LINE of S;
predA on L means :Def1: :: INCSP_1:def 1
[A,L] in the Inc of S;
end;

:: deftheorem Def1 defines on INCSP_1:def_1_:_
 for S being IncProjStr
for A being POINT of S
for L being LINE of S holds
( A on L iff [A,L] in the Inc of S );

definition
let S be IncStruct ;
let A be POINT of S;
let P be PLANE of S;
predA on P means :Def2: :: INCSP_1:def 2
[A,P] in the Inc2 of S;
end;

:: deftheorem Def2 defines on INCSP_1:def_2_:_
 for S being IncStruct
for A being POINT of S
for P being PLANE of S holds
( A on P iff [A,P] in the Inc2 of S );

definition
let S be IncStruct ;
let L be LINE of S;
let P be PLANE of S;
predL on P means :Def3: :: INCSP_1:def 3
[L,P] in the Inc3 of S;
end;

:: deftheorem Def3 defines on INCSP_1:def_3_:_
 for S being IncStruct
for L being LINE of S
for P being PLANE of S holds
( L on P iff [L,P] in the Inc3 of S );

definition
let S be IncProjStr ;
let F be Subset of the Points of S;
let L be LINE of S;
predF on L means :Def4: :: INCSP_1:def 4
 for A being POINT of S st A in F holds
A on L;
end;

:: deftheorem Def4 defines on INCSP_1:def_4_:_
 for S being IncProjStr
for F being Subset of the Points of S
for L being LINE of S holds
( F on L iff for A being POINT of S st A in F holds
A on L );

definition
let S be IncStruct ;
let F be Subset of the Points of S;
let P be PLANE of S;
predF on P means :Def5: :: INCSP_1:def 5
 for A being POINT of S st A in F holds
A on P;
end;

:: deftheorem Def5 defines on INCSP_1:def_5_:_
 for S being IncStruct
for F being Subset of the Points of S
for P being PLANE of S holds
( F on P iff for A being POINT of S st A in F holds
A on P );

definition
let S be IncProjStr ;
let F be Subset of the Points of S;
attrF is linear  means :Def6: :: INCSP_1:def 6
 ex L being LINE of S st F on L;
end;

:: deftheorem Def6 defines linear INCSP_1:def_6_:_
 for S being IncProjStr
for F being Subset of the Points of S holds
( F is linear iff ex L being LINE of S st F on L );

definition
let S be IncStruct ;
let F be Subset of the Points of S;
attrF is planar  means :Def7: :: INCSP_1:def 7
 ex P being PLANE of S st F on P;
end;

:: deftheorem Def7 defines planar INCSP_1:def_7_:_
 for S being IncStruct
for F being Subset of the Points of S holds
( F is planar iff ex P being PLANE of S st F on P );

theorem Th1: :: INCSP_1:1
for S being IncProjStr
for L being LINE of S
for A, B being POINT of S holds
( {A,B} on L iff ( A on L & B on L ) )
proof
let S be IncProjStr ; ::_thesis: for L being LINE of S
for A, B being POINT of S holds
( {A,B} on L iff ( A on L & B on L ) )
let L be LINE of S; ::_thesis: for A, B being POINT of S holds
( {A,B} on L iff ( A on L & B on L ) )
let A, B be POINT of S; ::_thesis: ( {A,B} on L iff ( A on L & B on L ) )
thus  ( {A,B} on L implies ( A on L & B on L ) ) ::_thesis: ( A on L & B on L implies {A,B} on L )
proof
A1: ( A in {A,B} & B in {A,B} ) by TARSKI:def_2;
assume  {A,B} on L ; ::_thesis: ( A on L & B on L )
hence  ( A on L & B on L ) by A1, Def4; ::_thesis: verum
end;
assume A2: ( A on L & B on L ) ; ::_thesis: {A,B} on L
let C be POINT of S; :: according to INCSP_1:def_4 ::_thesis: ( C in {A,B} implies C on L )
assume  C in {A,B} ; ::_thesis: C on L
hence  C on L by A2, TARSKI:def_2; ::_thesis: verum
end;

theorem Th2: :: INCSP_1:2
for S being IncProjStr
for L being LINE of S
for A, B, C being POINT of S holds
( {A,B,C} on L iff ( A on L & B on L & C on L ) )
proof
let S be IncProjStr ; ::_thesis: for L being LINE of S
for A, B, C being POINT of S holds
( {A,B,C} on L iff ( A on L & B on L & C on L ) )
let L be LINE of S; ::_thesis: for A, B, C being POINT of S holds
( {A,B,C} on L iff ( A on L & B on L & C on L ) )
let A, B, C be POINT of S; ::_thesis: ( {A,B,C} on L iff ( A on L & B on L & C on L ) )
thus  ( {A,B,C} on L implies ( A on L & B on L & C on L ) ) ::_thesis: ( A on L & B on L & C on L implies {A,B,C} on L )
proof
A1: C in {A,B,C} by ENUMSET1:def_1;
A2: ( A in {A,B,C} & B in {A,B,C} ) by ENUMSET1:def_1;
assume  {A,B,C} on L ; ::_thesis: ( A on L & B on L & C on L )
hence  ( A on L & B on L & C on L ) by A2, A1, Def4; ::_thesis: verum
end;
assume A3: ( A on L & B on L & C on L ) ; ::_thesis: {A,B,C} on L
let D be POINT of S; :: according to INCSP_1:def_4 ::_thesis: ( D in {A,B,C} implies D on L )
assume  D in {A,B,C} ; ::_thesis: D on L
hence  D on L by A3, ENUMSET1:def_1; ::_thesis: verum
end;

theorem Th3: :: INCSP_1:3
for S being IncStruct
for A, B being POINT of S
for P being PLANE of S holds
( {A,B} on P iff ( A on P & B on P ) )
proof
let S be IncStruct ; ::_thesis: for A, B being POINT of S
for P being PLANE of S holds
( {A,B} on P iff ( A on P & B on P ) )
let A, B be POINT of S; ::_thesis: for P being PLANE of S holds
( {A,B} on P iff ( A on P & B on P ) )
let P be PLANE of S; ::_thesis: ( {A,B} on P iff ( A on P & B on P ) )
thus  ( {A,B} on P implies ( A on P & B on P ) ) ::_thesis: ( A on P & B on P implies {A,B} on P )
proof
A1: ( A in {A,B} & B in {A,B} ) by TARSKI:def_2;
assume  {A,B} on P ; ::_thesis: ( A on P & B on P )
hence  ( A on P & B on P ) by A1, Def5; ::_thesis: verum
end;
assume A2: ( A on P & B on P ) ; ::_thesis: {A,B} on P
let C be POINT of S; :: according to INCSP_1:def_5 ::_thesis: ( C in {A,B} implies C on P )
assume  C in {A,B} ; ::_thesis: C on P
hence  C on P by A2, TARSKI:def_2; ::_thesis: verum
end;

theorem Th4: :: INCSP_1:4
for S being IncStruct
for A, B, C being POINT of S
for P being PLANE of S holds
( {A,B,C} on P iff ( A on P & B on P & C on P ) )
proof
let S be IncStruct ; ::_thesis: for A, B, C being POINT of S
for P being PLANE of S holds
( {A,B,C} on P iff ( A on P & B on P & C on P ) )
let A, B, C be POINT of S; ::_thesis: for P being PLANE of S holds
( {A,B,C} on P iff ( A on P & B on P & C on P ) )
let P be PLANE of S; ::_thesis: ( {A,B,C} on P iff ( A on P & B on P & C on P ) )
thus  ( {A,B,C} on P implies ( A on P & B on P & C on P ) ) ::_thesis: ( A on P & B on P & C on P implies {A,B,C} on P )
proof
A1: C in {A,B,C} by ENUMSET1:def_1;
A2: ( A in {A,B,C} & B in {A,B,C} ) by ENUMSET1:def_1;
assume  {A,B,C} on P ; ::_thesis: ( A on P & B on P & C on P )
hence  ( A on P & B on P & C on P ) by A2, A1, Def5; ::_thesis: verum
end;
assume A3: ( A on P & B on P & C on P ) ; ::_thesis: {A,B,C} on P
let D be POINT of S; :: according to INCSP_1:def_5 ::_thesis: ( D in {A,B,C} implies D on P )
assume  D in {A,B,C} ; ::_thesis: D on P
hence  D on P by A3, ENUMSET1:def_1; ::_thesis: verum
end;

theorem Th5: :: INCSP_1:5
for S being IncStruct
for A, B, C, D being POINT of S
for P being PLANE of S holds
( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )
proof
let S be IncStruct ; ::_thesis: for A, B, C, D being POINT of S
for P being PLANE of S holds
( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )
let A, B, C, D be POINT of S; ::_thesis: for P being PLANE of S holds
( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )
let P be PLANE of S; ::_thesis: ( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )
thus  ( {A,B,C,D} on P implies ( A on P & B on P & C on P & D on P ) ) ::_thesis: ( A on P & B on P & C on P & D on P implies {A,B,C,D} on P )
proof
A1: ( C in {A,B,C,D} & D in {A,B,C,D} ) by ENUMSET1:def_2;
A2: ( A in {A,B,C,D} & B in {A,B,C,D} ) by ENUMSET1:def_2;
assume  {A,B,C,D} on P ; ::_thesis: ( A on P & B on P & C on P & D on P )
hence  ( A on P & B on P & C on P & D on P ) by A2, A1, Def5; ::_thesis: verum
end;
assume A3: ( A on P & B on P & C on P & D on P ) ; ::_thesis: {A,B,C,D} on P
let E be POINT of S; :: according to INCSP_1:def_5 ::_thesis: ( E in {A,B,C,D} implies E on P )
assume  E in {A,B,C,D} ; ::_thesis: E on P
hence  E on P by A3, ENUMSET1:def_2; ::_thesis: verum
end;

theorem Th6: :: INCSP_1:6
for S being IncStruct
for L being LINE of S
for G, F being Subset of the Points of S st G c= F & F on L holds
G on L
proof
let S be IncStruct ; ::_thesis: for L being LINE of S
for G, F being Subset of the Points of S st G c= F & F on L holds
G on L
let L be LINE of S; ::_thesis: for G, F being Subset of the Points of S st G c= F & F on L holds
G on L
let G, F be Subset of the Points of S; ::_thesis: ( G c= F & F on L implies G on L )
assume A1: ( G c= F & F on L ) ; ::_thesis: G on L
let A be POINT of S; :: according to INCSP_1:def_4 ::_thesis: ( A in G implies A on L )
assume  A in G ; ::_thesis: A on L
hence  A on L by A1, Def4; ::_thesis: verum
end;

theorem Th7: :: INCSP_1:7
for S being IncStruct
for P being PLANE of S
for G, F being Subset of the Points of S st G c= F & F on P holds
G on P
proof
let S be IncStruct ; ::_thesis: for P being PLANE of S
for G, F being Subset of the Points of S st G c= F & F on P holds
G on P
let P be PLANE of S; ::_thesis: for G, F being Subset of the Points of S st G c= F & F on P holds
G on P
let G, F be Subset of the Points of S; ::_thesis: ( G c= F & F on P implies G on P )
assume A1: ( G c= F & F on P ) ; ::_thesis: G on P
let A be POINT of S; :: according to INCSP_1:def_5 ::_thesis: ( A in G implies A on P )
assume  A in G ; ::_thesis: A on P
hence  A on P by A1, Def5; ::_thesis: verum
end;

theorem Th8: :: INCSP_1:8
for S being IncStruct
for A being POINT of S
for L being LINE of S
for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )
proof
let S be IncStruct ; ::_thesis: for A being POINT of S
for L being LINE of S
for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )
let A be POINT of S; ::_thesis: for L being LINE of S
for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )
let L be LINE of S; ::_thesis: for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )
let F be Subset of the Points of S; ::_thesis: ( ( F on L & A on L ) iff F \/ {A} on L )
thus  ( F on L & A on L implies F \/ {A} on L ) ::_thesis: ( F \/ {A} on L implies ( F on L & A on L ) )
proof
assume A1: ( F on L & A on L ) ; ::_thesis: F \/ {A} on L
let C be POINT of S; :: according to INCSP_1:def_4 ::_thesis: ( C in F \/ {A} implies C on L )
assume  C in F \/ {A} ; ::_thesis: C on L
then  ( C in F or C in {A} ) by XBOOLE_0:def_3;
hence  C on L by A1, Def4, TARSKI:def_1; ::_thesis: verum
end;
assume A2: F \/ {A} on L ; ::_thesis: ( F on L & A on L )
hence  F on L by Th6, XBOOLE_1:7; ::_thesis: A on L
 {A} c= F \/ {A} by XBOOLE_1:7;
then  {A,A} c= F \/ {A} by ENUMSET1:29;
then  {A,A} on L by A2, Th6;
hence  A on L by Th1; ::_thesis: verum
end;

theorem Th9: :: INCSP_1:9
for S being IncStruct
for A being POINT of S
for P being PLANE of S
for F being Subset of the Points of S holds
( ( F on P & A on P ) iff F \/ {A} on P )
proof
let S be IncStruct ; ::_thesis: for A being POINT of S
for P being PLANE of S
for F being Subset of the Points of S holds
( ( F on P & A on P ) iff F \/ {A} on P )
let A be POINT of S; ::_thesis: for P being PLANE of S
for F being Subset of the Points of S holds
( ( F on P & A on P ) iff F \/ {A} on P )
let P be PLANE of S; ::_thesis: for F being Subset of the Points of S holds
( ( F on P & A on P ) iff F \/ {A} on P )
let F be Subset of the Points of S; ::_thesis: ( ( F on P & A on P ) iff F \/ {A} on P )
thus  ( F on P & A on P implies F \/ {A} on P ) ::_thesis: ( F \/ {A} on P implies ( F on P & A on P ) )
proof
assume A1: ( F on P & A on P ) ; ::_thesis: F \/ {A} on P
let C be POINT of S; :: according to INCSP_1:def_5 ::_thesis: ( C in F \/ {A} implies C on P )
assume  C in F \/ {A} ; ::_thesis: C on P
then  ( C in F or C in {A} ) by XBOOLE_0:def_3;
hence  C on P by A1, Def5, TARSKI:def_1; ::_thesis: verum
end;
assume A2: F \/ {A} on P ; ::_thesis: ( F on P & A on P )
hence  F on P by Th7, XBOOLE_1:7; ::_thesis: A on P
 {A} c= F \/ {A} by XBOOLE_1:7;
then  {A,A} c= F \/ {A} by ENUMSET1:29;
then  {A,A} on P by A2, Th7;
hence  A on P by Th3; ::_thesis: verum
end;

theorem Th10: :: INCSP_1:10
for S being IncStruct
for L being LINE of S
for F, G being Subset of the Points of S holds
( F \/ G on L iff ( F on L & G on L ) )
proof
let S be IncStruct ; ::_thesis: for L being LINE of S
for F, G being Subset of the Points of S holds
( F \/ G on L iff ( F on L & G on L ) )
let L be LINE of S; ::_thesis: for F, G being Subset of the Points of S holds
( F \/ G on L iff ( F on L & G on L ) )
let F, G be Subset of the Points of S; ::_thesis: ( F \/ G on L iff ( F on L & G on L ) )
thus  ( F \/ G on L implies ( F on L & G on L ) ) by Th6, XBOOLE_1:7; ::_thesis: ( F on L & G on L implies F \/ G on L )
assume A1: ( F on L & G on L ) ; ::_thesis: F \/ G on L
let C be POINT of S; :: according to INCSP_1:def_4 ::_thesis: ( C in F \/ G implies C on L )
assume  C in F \/ G ; ::_thesis: C on L
then  ( C in F or C in G ) by XBOOLE_0:def_3;
hence  C on L by A1, Def4; ::_thesis: verum
end;

theorem Th11: :: INCSP_1:11
for S being IncStruct
for P being PLANE of S
for F, G being Subset of the Points of S holds
( F \/ G on P iff ( F on P & G on P ) )
proof
let S be IncStruct ; ::_thesis: for P being PLANE of S
for F, G being Subset of the Points of S holds
( F \/ G on P iff ( F on P & G on P ) )
let P be PLANE of S; ::_thesis: for F, G being Subset of the Points of S holds
( F \/ G on P iff ( F on P & G on P ) )
let F, G be Subset of the Points of S; ::_thesis: ( F \/ G on P iff ( F on P & G on P ) )
thus  ( F \/ G on P implies ( F on P & G on P ) ) by Th7, XBOOLE_1:7; ::_thesis: ( F on P & G on P implies F \/ G on P )
assume A1: ( F on P & G on P ) ; ::_thesis: F \/ G on P
let C be POINT of S; :: according to INCSP_1:def_5 ::_thesis: ( C in F \/ G implies C on P )
assume  C in F \/ G ; ::_thesis: C on P
then  ( C in F or C in G ) by XBOOLE_0:def_3;
hence  C on P by A1, Def5; ::_thesis: verum
end;

theorem :: INCSP_1:12
for S being IncStruct
for G, F being Subset of the Points of S st G c= F & F is linear holds
G is linear
proof
let S be IncStruct ; ::_thesis: for G, F being Subset of the Points of S st G c= F & F is linear holds
G is linear
let G, F be Subset of the Points of S; ::_thesis: ( G c= F & F is linear implies G is linear )
assume that
A1: G c= F and
A2: F is linear ; ::_thesis: G is linear
consider L being LINE of S such that
A3: F on L by A2, Def6;
take  L ; :: according to INCSP_1:def_6 ::_thesis: G on L
let A be POINT of S; :: according to INCSP_1:def_4 ::_thesis: ( A in G implies A on L )
assume  A in G ; ::_thesis: A on L
hence  A on L by A1, A3, Def4; ::_thesis: verum
end;

theorem :: INCSP_1:13
for S being IncStruct
for G, F being Subset of the Points of S st G c= F & F is planar holds
G is planar
proof
let S be IncStruct ; ::_thesis: for G, F being Subset of the Points of S st G c= F & F is planar holds
G is planar
let G, F be Subset of the Points of S; ::_thesis: ( G c= F & F is planar implies G is planar )
assume that
A1: G c= F and
A2: F is planar ; ::_thesis: G is planar
consider P being PLANE of S such that
A3: F on P by A2, Def7;
take  P ; :: according to INCSP_1:def_7 ::_thesis: G on P
let A be POINT of S; :: according to INCSP_1:def_5 ::_thesis: ( A in G implies A on P )
assume  A in G ; ::_thesis: A on P
hence  A on P by A1, A3, Def5; ::_thesis: verum
end;

definition
let S be IncProjStr ;
attrS is with_non-trivial_lines  means :Def8: :: INCSP_1:def 8
 for L being LINE of S ex A, B being POINT of S st
( A <> B & {A,B} on L );
attrS is linear  means :Def9: :: INCSP_1:def 9
 for A, B being POINT of S ex L being LINE of S st {A,B} on L;
attrS is up-2-rank  means :Def10: :: INCSP_1:def 10
 for A, B being POINT of S
for K, L being LINE of S st A <> B & {A,B} on K & {A,B} on L holds
K = L;
end;

:: deftheorem Def8 defines with_non-trivial_lines INCSP_1:def_8_:_
 for S being IncProjStr holds
( S is with_non-trivial_lines iff for L being LINE of S ex A, B being POINT of S st
( A <> B & {A,B} on L ) );

:: deftheorem Def9 defines linear INCSP_1:def_9_:_
 for S being IncProjStr holds
( S is linear iff for A, B being POINT of S ex L being LINE of S st {A,B} on L );

:: deftheorem Def10 defines up-2-rank INCSP_1:def_10_:_
 for S being IncProjStr holds
( S is up-2-rank iff for A, B being POINT of S
for K, L being LINE of S st A <> B & {A,B} on K & {A,B} on L holds
K = L );

definition
let S be IncStruct ;
attrS is with_non-empty_planes  means :Def11: :: INCSP_1:def 11
 for P being PLANE of S ex A being POINT of S st A on P;
attrS is planar  means :Def12: :: INCSP_1:def 12
 for A, B, C being POINT of S ex P being PLANE of S st {A,B,C} on P;
attrS is with_<=1_plane_per_3_pts  means :Def13: :: INCSP_1:def 13
 for A, B, C being POINT of S
for P, Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Q;
attrS is with_lines_inside_planes  means :Def14: :: INCSP_1:def 14
 for L being LINE of S
for P being PLANE of S st ex A, B being POINT of S st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P;
attrS is with_planes_intersecting_in_2_pts  means :Def15: :: INCSP_1:def 15
 for A being POINT of S
for P, Q being PLANE of S st A on P & A on Q holds
ex B being POINT of S st
( A <> B & B on P & B on Q );
attrS is up-3-dimensional  means :Def16: :: INCSP_1:def 16
 not for A, B, C, D being POINT of S holds {A,B,C,D} is planar ;
attrS is inc-compatible  means :Def17: :: INCSP_1:def 17
 for A being POINT of S
for L being LINE of S
for P being PLANE of S st A on L & L on P holds
A on P;
end;

:: deftheorem Def11 defines with_non-empty_planes INCSP_1:def_11_:_
 for S being IncStruct holds
( S is with_non-empty_planes iff for P being PLANE of S ex A being POINT of S st A on P );

:: deftheorem Def12 defines planar INCSP_1:def_12_:_
 for S being IncStruct holds
( S is planar iff for A, B, C being POINT of S ex P being PLANE of S st {A,B,C} on P );

:: deftheorem Def13 defines with_<=1_plane_per_3_pts INCSP_1:def_13_:_
 for S being IncStruct holds
( S is with_<=1_plane_per_3_pts iff for A, B, C being POINT of S
for P, Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Q );

:: deftheorem Def14 defines with_lines_inside_planes INCSP_1:def_14_:_
 for S being IncStruct holds
( S is with_lines_inside_planes iff for L being LINE of S
for P being PLANE of S st ex A, B being POINT of S st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P );

:: deftheorem Def15 defines with_planes_intersecting_in_2_pts INCSP_1:def_15_:_
 for S being IncStruct holds
( S is with_planes_intersecting_in_2_pts iff for A being POINT of S
for P, Q being PLANE of S st A on P & A on Q holds
ex B being POINT of S st
( A <> B & B on P & B on Q ) );

:: deftheorem Def16 defines up-3-dimensional INCSP_1:def_16_:_
 for S being IncStruct holds
( S is up-3-dimensional iff not for A, B, C, D being POINT of S holds {A,B,C,D} is planar );

:: deftheorem Def17 defines inc-compatible INCSP_1:def_17_:_
 for S being IncStruct holds
( S is inc-compatible iff for A being POINT of S
for L being LINE of S
for P being PLANE of S st A on L & L on P holds
A on P );

definition
let IT be IncStruct ;
attrIT is IncSpace-like  means :Def18: :: INCSP_1:def 18
( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is with_non-empty_planes & IT is planar & IT is with_<=1_plane_per_3_pts & IT is with_lines_inside_planes & IT is with_planes_intersecting_in_2_pts & IT is up-3-dimensional & IT is inc-compatible );
end;

:: deftheorem Def18 defines IncSpace-like INCSP_1:def_18_:_
 for IT being IncStruct holds
( IT is IncSpace-like iff ( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is with_non-empty_planes & IT is planar & IT is with_<=1_plane_per_3_pts & IT is with_lines_inside_planes & IT is with_planes_intersecting_in_2_pts & IT is up-3-dimensional & IT is inc-compatible ) );


registration
cluster IncSpace-like  ->  with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible for IncStruct ;
coherence
 for b1 being IncStruct st b1 is IncSpace-like holds
( b1 is with_non-trivial_lines & b1 is linear & b1 is up-2-rank & b1 is with_non-empty_planes & b1 is planar & b1 is with_<=1_plane_per_3_pts & b1 is with_lines_inside_planes & b1 is with_planes_intersecting_in_2_pts & b1 is up-3-dimensional & b1 is inc-compatible ) by Def18;
end;

registration
cluster strict IncSpace-like for IncStruct ;
existence
 ex b1 being IncStruct st
( b1 is strict & b1 is IncSpace-like )
proof
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 set ; :: 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 set ; :: 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 set ; :: 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 A1, TARSKI:def_2;
then  [b,l] in i1 ;
then A3: B on L by Def1;
 a in l by A1, TARSKI:def_2;
then  [a,l] in i1 ;
then  A on L by Def1;
hence  {A,B} on L by A3, Th1; ::_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 A6, ENUMSET1:def_2; ::_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 A8, TARSKI:def_2;
then  [a,l] in i1 ;
then A9: A on L by Def1;
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;
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 A10, TARSKI:def_2;
then  [b,l] in i1 ;
then A11: B on L by Def1;
 a in l by A10, TARSKI:def_2;
then  [a,l] in i1 ;
then  A on L by Def1;
then  {A,B} on L by A11, 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;
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 A13, XTUPLE_0:1;
hence  a in l by A13, A14, XTUPLE_0:1; ::_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 A16, Th1;
then  [b,k] in i1 by Def1;
then  b in k by A12;
then A19: ( b = x1 or b = x2 ) by A18, TARSKI:def_2;
 l in Li ;
then consider x3, x4 being Element of {0,1,2,3} such that
A20: l = {x3,x4} and
 x3 <> x4 ;
 A on L by A17, Th1;
then  [a,l] in i1 by Def1;
then  a in l by A12;
then A21: ( a = x3 or a = x4 ) by A20, TARSKI:def_2;
 B on L by A17, Th1;
then  [b,l] in i1 by Def1;
then A22: b in l by A12;
 A on K by A16, Th1;
then  [a,k] in i1 by Def1;
then  a in k by A12;
then  ( a = x1 or a = x2 ) by A18, TARSKI:def_2;
hence  K = L by A15, A22, A18, A19, A20, A21, TARSKI:def_2; ::_thesis: 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 A23, ENUMSET1:def_1;
then  [a,p] in i2 ;
hence  A on P by Def2; ::_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 A25, ENUMSET1:def_2; ::_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 A27, ENUMSET1:def_1;
then  [a,p] in i2 ;
then  A on P by Def2;
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;
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 A33, A36, A42, A39, ENUMSET1:def_2; ::_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 A32, A47;
then consider p being Element of Pl such that
A48: p = {x,y,z} ;
reconsider P = p as PLANE of IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) ;
 b in p by A30, A31, A32, A48, ENUMSET1:def_1;
then  [b,p] in i2 ;
then A49: B on P by Def2;
 c in p by A30, A31, A32, A48, ENUMSET1:def_1;
then  [c,p] in i2 ;
then A50: C on P by Def2;
 a in p by A30, A31, A32, A48, ENUMSET1:def_1;
then  [a,p] in i2 ;
then  A on P by Def2;
then  {A,B,C} on P by A49, A50, 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;
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 A51, ENUMSET1:def_1;
then  [b,p] in i2 ;
then A52: B on P by Def2;
 c in p by A51, ENUMSET1:def_1;
then  [c,p] in i2 ;
then A53: C on P by Def2;
 a in p by A51, ENUMSET1:def_1;
then  [a,p] in i2 ;
then  A on P by Def2;
then  {A,B,C} on P by A52, A53, 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;
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: 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 A55, XTUPLE_0:1;
hence  a in p by A55, A56, XTUPLE_0:1; ::_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 A58, Th4;
then  [a,p] in i2 by Def2;
then  a in p by A54;
then A61: ( a = x1 or a = x2 or a = x3 ) by A60, ENUMSET1:def_1;
 C on P by A58, Th4;
then  [c,p] in i2 by Def2;
then  c in p by A54;
then A62: ( c = x1 or c = x2 or c = x3 ) by A60, ENUMSET1:def_1;
 B on P by A58, Th4;
then  [b,p] in i2 by Def2;
then  b in p by A54;
then A63: ( b = x1 or b = x2 or b = x3 ) by A60, ENUMSET1:def_1;
 q in Pl ;
then consider x1, x2, x3 being Element of {0,1,2,3} such that
A64: q = {x1,x2,x3} and
 x1 <> x2 and
 x1 <> x3 and
 x2 <> x3 ;
 B on Q by A59, Th4;
then  [b,q] in i2 by Def2;
then  b in q by A54;
then A65: ( b = x1 or b = x2 or b = x3 ) by A64, ENUMSET1:def_1;
A66: now__::_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, Def9;
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, Def9;
A70: ( not {A,B,C} on K & not {A,B,C} on L ) by A57, Def6;
assume A71: ( A = B or A = C or B = C ) ; ::_thesis: contradiction
 ( A on K & B on K ) by A69, Th1;
hence  contradiction by A71, A68, A70, Th2; ::_thesis: verum
end;
 C on Q by A59, Th4;
then  [c,q] in i2 by Def2;
then  c in q by A54;
then A72: ( c = x1 or c = x2 or c = x3 ) by A64, ENUMSET1:def_1;
 A on Q by A59, Th4;
then  [a,q] in i2 by Def2;
then  a in q by A54;
then  ( a = x1 or a = x2 or a = x3 ) by A64, ENUMSET1:def_1;
hence  P = Q by A66, A60, A61, A63, A62, A64, A65, A72, ENUMSET1:57, ENUMSET1:58, ENUMSET1:59, ENUMSET1:60; ::_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 A75, Th3;
then  [a,p] in i2 by Def2;
then A76: a in p by A54;
reconsider l = L as Element of Li ;
 B on L by A74, Th1;
then  [b,l] in i1 by Def1;
then A77: b in l by A12;
 B on P by A75, Th3;
then  [b,p] in i2 by Def2;
then A78: b in p by A54;
 A on L by A74, Th1;
then  [a,l] in i1 by Def1;
then A79: a in l by A12;
now__::_thesis:_for_x_being_set_st_x_in_l_holds_
x_in_p
let x be set ; ::_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;
then  l c= p by TARSKI:def_3;
then  [l,p] in i3 ;
hence  L on P by Def3; ::_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 A85, ENUMSET1:def_1;
A88: x3 in p by A85, ENUMSET1:def_1;
 q in Pl ;
then consider y1, y2, y3 being Element of {0,1,2,3} such that
A89: q = {y1,y2,y3} and
A90: ( y1 <> y2 & y1 <> y3 & y2 <> y3 ) ;
A91: ( y1 in q & y2 in q ) by A89, ENUMSET1:def_1;
A92: y3 in q by A89, ENUMSET1:def_1;
 [a,q] in i2 by A84, Def2;
then  a in q by A54;
then  ( a = y1 or a = y2 or a = y3 ) by A89, ENUMSET1:def_1;
then consider z3, z4 being Element of {0,1,2,3} such that
A93: ( z3 in q & z4 in q ) and
A94: z3 <> a and
A95: ( z4 <> a & z3 <> z4 ) by A90, A91, A92;
 [a,p] in i2 by A83, Def2;
then  a in p by A54;
then  ( a = x1 or a = x2 or a = x3 ) by A85, ENUMSET1:def_1;
then consider z1, z2 being Element of {0,1,2,3} such that
A96: ( z1 in p & z2 in p ) and
A97: z1 <> a and
A98: z2 <> a and
A99: z1 <> z2 by A86, A87, A88;
now__::_thesis:_(_z1_<>_z3_&_z1_<>_z4_&_z2_<>_z3_implies_not_z2_<>_z4_)
assume A100: ( z1 <> z3 & z1 <> z4 & z2 <> z3 & z2 <> z4 ) ; ::_thesis: contradiction
percases ( a = 0 or a = 1 or a = 2 or a = 3 ) by ENUMSET1:def_2;
supposeA101: 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;
supposeA104: 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;
supposeA107: 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;
supposeA110: 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;
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 ) by Def2; ::_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 by Def7;
reconsider p = P as Element of Pl ;
 p in Pl ;
then consider a, b, c being Element of {0,1,2,3} such that
A116: p = {a,b,c} and
 a <> b and
 a <> c and
 b <> c ;
 D on P by A115, Th5;
then  [Three,p] in i2 by Def2;
then A117: Three in p by A54;
 C on P by A115, Th5;
then  [Two,p] in i2 by Def2;
then  Two in p by A54;
then A118: ( Two = a or Two = b or Two = c ) by A116, ENUMSET1:def_1;
 B on P by A115, Th5;
then  [One,p] in i2 by Def2;
then  One in p by A54;
then A119: ( One = a or One = b or One = c ) by A116, ENUMSET1:def_1;
 A on P by A115, Th5;
then  [Zero1,p] in i2 by Def2;
then  Zero1 in p by A54;
then  ( Zero1 = a or Zero1 = b or Zero1 = c ) by A116, ENUMSET1:def_1;
hence  contradiction by A116, A117, A119, A118, ENUMSET1:def_1; ::_thesis: 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 A121, XTUPLE_0:1;
hence  l c= p by A121, A122, XTUPLE_0:1; ::_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, Def3;
then A125: l c= p by A120;
 [a,l] in i1 by A123, Def1;
then  a in l by A12;
then  [a,p] in i2 by A125;
hence  A on P by Def2; ::_thesis: verum
end;
end;
then  IncStruct(# {0,1,2,3},Li,Pl,i1,i2,i3 #) is IncSpace-like by Def18;
hence  ex b1 being IncStruct st
( b1 is strict & b1 is IncSpace-like ) ; ::_thesis: verum
end;
end;

definition
mode IncSpace is IncSpace-like IncStruct ;
end;


theorem Th14: :: INCSP_1:14
for S being IncSpace
for L being LINE of S
for P being PLANE of S
for F being Subset of the Points of S st F on L & L on P holds
F on P
proof
let S be IncSpace; ::_thesis: for L being LINE of S
for P being PLANE of S
for F being Subset of the Points of S st F on L & L on P holds
F on P
let L be LINE of S; ::_thesis: for P being PLANE of S
for F being Subset of the Points of S st F on L & L on P holds
F on P
let P be PLANE of S; ::_thesis: for F being Subset of the Points of S st F on L & L on P holds
F on P
let F be Subset of the Points of S; ::_thesis: ( F on L & L on P implies F on P )
assume that
A1: F on L and
A2: L on P ; ::_thesis: F on P
let A be POINT of S; :: according to INCSP_1:def_5 ::_thesis: ( A in F implies A on P )
assume  A in F ; ::_thesis: A on P
then  A on L by A1, Def4;
hence  A on P by A2, Def17; ::_thesis: verum
end;

theorem Th15: :: INCSP_1:15
for S being IncSpace
for A, B being POINT of S holds {A,A,B} is linear
proof
let S be IncSpace; ::_thesis: for A, B being POINT of S holds {A,A,B} is linear
let A, B be POINT of S; ::_thesis: {A,A,B} is linear
consider K being LINE of S such that
A1: {A,B} on K by Def9;
take  K ; :: according to INCSP_1:def_6 ::_thesis: {A,A,B} on K
thus  {A,A,B} on K by A1, ENUMSET1:30; ::_thesis: verum
end;

theorem Th16: :: INCSP_1:16
for S being IncSpace
for A, B, C being POINT of S holds {A,A,B,C} is planar
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S holds {A,A,B,C} is planar
let A, B, C be POINT of S; ::_thesis: {A,A,B,C} is planar
consider P being PLANE of S such that
A1: {A,B,C} on P by Def12;
take  P ; :: according to INCSP_1:def_7 ::_thesis: {A,A,B,C} on P
thus  {A,A,B,C} on P by A1, ENUMSET1:31; ::_thesis: verum
end;

theorem Th17: :: INCSP_1:17
for S being IncSpace
for A, B, C, D being POINT of S st {A,B,C} is linear holds
{A,B,C,D} is planar
proof
let S be IncSpace; ::_thesis: for A, B, C, D being POINT of S st {A,B,C} is linear holds
{A,B,C,D} is planar
let A, B, C, D be POINT of S; ::_thesis: ( {A,B,C} is linear implies {A,B,C,D} is planar )
given L being LINE of S such that A1: {A,B,C} on L ; :: according to INCSP_1:def_6 ::_thesis: {A,B,C,D} is planar
 {A,B} \/ {C} on L by A1, ENUMSET1:3;
then A2: {A,B} on L by Th8;
consider P being PLANE of S such that
A3: {A,B,D} on P by Def12;
 {A,B} \/ {D} on P by A3, ENUMSET1:3;
then A4: {A,B} on P by Th11;
assume A5: not {A,B,C,D} is planar ; ::_thesis: contradiction
then  A <> B by Th16;
then  L on P by A2, A4, Def14;
then A6: {A,B,C} on P by A1, Th14;
then A7: C on P by Th4;
A8: D on P by A3, Th4;
 ( A on P & B on P ) by A6, Th4;
then  {A,B,C,D} on P by A7, A8, Th5;
hence  contradiction by A5, Def7; ::_thesis: verum
end;

theorem Th18: :: INCSP_1:18
for S being IncSpace
for A, B, C being POINT of S
for L being LINE of S st A <> B & {A,B} on L & not C on L holds
not {A,B,C} is linear
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S
for L being LINE of S st A <> B & {A,B} on L & not C on L holds
not {A,B,C} is linear
let A, B, C be POINT of S; ::_thesis: for L being LINE of S st A <> B & {A,B} on L & not C on L holds
not {A,B,C} is linear
let L be LINE of S; ::_thesis: ( A <> B & {A,B} on L & not C on L implies not {A,B,C} is linear )
assume that
A1: ( A <> B & {A,B} on L ) and
A2: not C on L ; ::_thesis: not {A,B,C} is linear
given K being LINE of S such that A3: {A,B,C} on K ; :: according to INCSP_1:def_6 ::_thesis: contradiction
 {A,B} \/ {C} on K by A3, ENUMSET1:3;
then  {A,B} on K by Th10;
then  L = K by A1, Def10;
hence  contradiction by A2, A3, Th2; ::_thesis: verum
end;

theorem Th19: :: INCSP_1:19
for S being IncSpace
for A, B, C, D being POINT of S
for P being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & not D on P holds
not {A,B,C,D} is planar
proof
let S be IncSpace; ::_thesis: for A, B, C, D being POINT of S
for P being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & not D on P holds
not {A,B,C,D} is planar
let A, B, C, D be POINT of S; ::_thesis: for P being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & not D on P holds
not {A,B,C,D} is planar
let P be PLANE of S; ::_thesis: ( not {A,B,C} is linear & {A,B,C} on P & not D on P implies not {A,B,C,D} is planar )
assume that
A1: ( not {A,B,C} is linear & {A,B,C} on P ) and
A2: not D on P ; ::_thesis: not {A,B,C,D} is planar
given Q being PLANE of S such that A3: {A,B,C,D} on Q ; :: according to INCSP_1:def_7 ::_thesis: contradiction
 {A,B,C} \/ {D} on Q by A3, ENUMSET1:6;
then  {A,B,C} on Q by Th9;
then  P = Q by A1, Def13;
hence  contradiction by A2, A3, Th5; ::_thesis: verum
end;

theorem :: INCSP_1:20
for S being IncSpace
for K, L being LINE of S st ( for P being PLANE of S holds
( not K on P or not L on P ) ) holds
K <> L
proof
let S be IncSpace; ::_thesis: for K, L being LINE of S st ( for P being PLANE of S holds
( not K on P or not L on P ) ) holds
K <> L
let K, L be LINE of S; ::_thesis: ( ( for P being PLANE of S holds
( not K on P or not L on P ) ) implies K <> L )
assume that
A1: for P being PLANE of S holds
( not K on P or not L on P ) and
A2: K = L ; ::_thesis: contradiction
consider A, B being POINT of S such that
A3: A <> B and
A4: {A,B} on K by Def8;
A5: ( A on K & B on K ) by A4, Th1;
consider C, D being POINT of S such that
A6: C <> D and
A7: {C,D} on L by Def8;
 C on K by A2, A7, Th1;
then  {A,B,C} on K by A5, Th2;
then  {A,B,C} is linear by Def6;
then  {A,B,C,D} is planar by Th17;
then consider Q being PLANE of S such that
A8: {A,B,C,D} on Q by Def7;
 ( C on Q & D on Q ) by A8, Th5;
then  {C,D} on Q by Th3;
then A9: L on Q by A6, A7, Def14;
 ( A on Q & B on Q ) by A8, Th5;
then  {A,B} on Q by Th3;
then  K on Q by A3, A4, Def14;
hence  contradiction by A1, A9; ::_thesis: verum
end;

Lm1:  for S being IncSpace
for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L )
proof
let S be IncSpace; ::_thesis: for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L )
let A be POINT of S; ::_thesis: for L being LINE of S ex B being POINT of S st
( A <> B & B on L )
let L be LINE of S; ::_thesis: ex B being POINT of S st
( A <> B & B on L )
consider B, C being POINT of S such that
A1: B <> C and
A2: {B,C} on L by Def8;
A3: ( A <> C or A <> B ) by A1;
 ( B on L & C on L ) by A2, Th1;
hence  ex B being POINT of S st
( A <> B & B on L ) by A3; ::_thesis: verum
end;

theorem :: INCSP_1:21
for S being IncSpace
for L, L1, L2 being LINE of S st ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st
( A on L & A on L1 & A on L2 ) holds
L <> L1
proof
let S be IncSpace; ::_thesis: for L, L1, L2 being LINE of S st ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st
( A on L & A on L1 & A on L2 ) holds
L <> L1
let L, L1, L2 be LINE of S; ::_thesis: ( ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st
( A on L & A on L1 & A on L2 ) implies L <> L1 )
assume A1: for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ; ::_thesis: ( for A being POINT of S holds
( not A on L or not A on L1 or not A on L2 ) or L <> L1 )
given A being POINT of S such that A2: A on L and
A3: A on L1 and
A4: A on L2 ; ::_thesis: L <> L1
consider C being POINT of S such that
A5: A <> C and
A6: C on L1 by Lm1;
consider D being POINT of S such that
A7: A <> D and
A8: D on L2 by Lm1;
consider B being POINT of S such that
A9: A <> B and
A10: B on L by Lm1;
assume A11: L = L1 ; ::_thesis: contradiction
then  {A,C,B} on L1 by A3, A10, A6, Th2;
then  {A,C} \/ {B} on L1 by ENUMSET1:3;
then A12: {A,C} on L1 by Th10;
 {A,B,C} on L by A3, A11, A10, A6, Th2;
then  {A,B,C} is linear by Def6;
then  {A,B,C,D} is planar by Th17;
then consider Q being PLANE of S such that
A13: {A,B,C,D} on Q by Def7;
 ( A on Q & D on Q ) by A13, Th5;
then A14: {A,D} on Q by Th3;
 {A,D} on L2 by A4, A8, Th1;
then A15: L2 on Q by A7, A14, Def14;
 ( A on Q & C on Q ) by A13, Th5;
then  {A,C} on Q by Th3;
then A16: L1 on Q by A5, A12, Def14;
 {A,B} \/ {C,D} on Q by A13, ENUMSET1:5;
then A17: {A,B} on Q by Th11;
 {A,B} on L by A2, A10, Th1;
then  L on Q by A9, A17, Def14;
hence  contradiction by A1, A16, A15; ::_thesis: verum
end;

theorem :: INCSP_1:22
for S being IncSpace
for L1, L2, L being LINE of S
for P being PLANE of S st L1 on P & L2 on P & not L on P & L1 <> L2 holds
for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
proof
let S be IncSpace; ::_thesis: for L1, L2, L being LINE of S
for P being PLANE of S st L1 on P & L2 on P & not L on P & L1 <> L2 holds
for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
let L1, L2, L be LINE of S; ::_thesis: for P being PLANE of S st L1 on P & L2 on P & not L on P & L1 <> L2 holds
for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
let P be PLANE of S; ::_thesis: ( L1 on P & L2 on P & not L on P & L1 <> L2 implies for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q ) )
assume that
A1: L1 on P and
A2: L2 on P and
A3: not L on P and
A4: L1 <> L2 ; ::_thesis: for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
consider A, B being POINT of S such that
A5: A <> B and
A6: {A,B} on L1 by Def8;
A7: {A,B} on P by A1, A6, Th14;
consider C, C1 being POINT of S such that
A8: C <> C1 and
A9: {C,C1} on L2 by Def8;
A10: now__::_thesis:_(_C_on_L1_implies_not_C1_on_L1_)
assume  ( C on L1 & C1 on L1 ) ; ::_thesis: contradiction
then  {C,C1} on L1 by Th1;
hence  contradiction by A4, A8, A9, Def10; ::_thesis: verum
end;
A11: {C,C1} on P by A2, A9, Th14;
then  C on P by Th3;
then  {A,B} \/ {C} on P by A7, Th9;
then A12: {A,B,C} on P by ENUMSET1:3;
 C1 on P by A11, Th3;
then  {A,B} \/ {C1} on P by A7, Th9;
then A13: {A,B,C1} on P by ENUMSET1:3;
consider D, E being POINT of S such that
A14: D <> E and
A15: {D,E} on L by Def8;
given Q being PLANE of S such that A16: L on Q and
A17: L1 on Q and
A18: L2 on Q ; ::_thesis: contradiction
A19: {A,B} on Q by A17, A6, Th14;
A20: {C,C1} on Q by A18, A9, Th14;
then A21: C on Q by Th3;
A22: {D,E} on Q by A16, A15, Th14;
then A23: D on Q by Th3;
then  {C,D} on Q by A21, Th3;
then  {A,B} \/ {C,D} on Q by A19, Th11;
then  {A,B,C,D} on Q by ENUMSET1:5;
then A24: {A,B,C,D} is planar by Def7;
A25: E on Q by A22, Th3;
then  {C,E} on Q by A21, Th3;
then  {A,B} \/ {C,E} on Q by A19, Th11;
then  {A,B,C,E} on Q by ENUMSET1:5;
then A26: {A,B,C,E} is planar by Def7;
A27: C1 on Q by A20, Th3;
then  {C1,D} on Q by A23, Th3;
then  {A,B} \/ {C1,D} on Q by A19, Th11;
then  {A,B,C1,D} on Q by ENUMSET1:5;
then A28: {A,B,C1,D} is planar by Def7;
 {C1,E} on Q by A27, A25, Th3;
then  {A,B} \/ {C1,E} on Q by A19, Th11;
then  {A,B,C1,E} on Q by ENUMSET1:5;
then A29: {A,B,C1,E} is planar by Def7;
 not {D,E} on P by A3, A14, A15, Def14;
then  ( not D on P or not E on P ) by Th3;
hence  contradiction by A5, A6, A24, A26, A28, A29, A10, A12, A13, Th18, Th19; ::_thesis: verum
end;

theorem Th23: :: INCSP_1:23
for S being IncSpace
for K, L being LINE of S st ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
( K on P & L on P )
proof
let S be IncSpace; ::_thesis: for K, L being LINE of S st ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
( K on P & L on P )
let K, L be LINE of S; ::_thesis: ( ex A being POINT of S st
( A on K & A on L ) implies ex P being PLANE of S st
( K on P & L on P ) )
given A being POINT of S such that A1: A on K and
A2: A on L ; ::_thesis: ex P being PLANE of S st
( K on P & L on P )
consider C being POINT of S such that
A3: A <> C and
A4: C on L by Lm1;
A5: {A,C} on L by A2, A4, Th1;
consider B being POINT of S such that
A6: A <> B and
A7: B on K by Lm1;
consider P being PLANE of S such that
A8: {A,B,C} on P by Def12;
take  P ; ::_thesis: ( K on P & L on P )
A9: A on P by A8, Th4;
 C on P by A8, Th4;
then A10: {A,C} on P by A9, Th3;
 B on P by A8, Th4;
then A11: {A,B} on P by A9, Th3;
 {A,B} on K by A1, A7, Th1;
hence  ( K on P & L on P ) by A6, A3, A5, A11, A10, Def14; ::_thesis: verum
end;

theorem :: INCSP_1:24
for S being IncSpace
for A, B being POINT of S st A <> B holds
ex L being LINE of S st
for K being LINE of S holds
( {A,B} on K iff K = L )
proof
let S be IncSpace; ::_thesis: for A, B being POINT of S st A <> B holds
ex L being LINE of S st
for K being LINE of S holds
( {A,B} on K iff K = L )
let A, B be POINT of S; ::_thesis: ( A <> B implies ex L being LINE of S st
for K being LINE of S holds
( {A,B} on K iff K = L ) )
assume A1: A <> B ; ::_thesis: ex L being LINE of S st
for K being LINE of S holds
( {A,B} on K iff K = L )
consider L being LINE of S such that
A2: {A,B} on L by Def9;
take  L ; ::_thesis: for K being LINE of S holds
( {A,B} on K iff K = L )
thus  for K being LINE of S holds
( {A,B} on K iff K = L ) by A1, A2, Def10; ::_thesis: verum
end;

theorem :: INCSP_1:25
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
ex P being PLANE of S st
for Q being PLANE of S holds
( {A,B,C} on Q iff P = Q )
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
ex P being PLANE of S st
for Q being PLANE of S holds
( {A,B,C} on Q iff P = Q )
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies ex P being PLANE of S st
for Q being PLANE of S holds
( {A,B,C} on Q iff P = Q ) )
assume A1: not {A,B,C} is linear ; ::_thesis: ex P being PLANE of S st
for Q being PLANE of S holds
( {A,B,C} on Q iff P = Q )
consider P being PLANE of S such that
A2: {A,B,C} on P by Def12;
take  P ; ::_thesis: for Q being PLANE of S holds
( {A,B,C} on Q iff P = Q )
thus  for Q being PLANE of S holds
( {A,B,C} on Q iff P = Q ) by A1, A2, Def13; ::_thesis: verum
end;

theorem Th26: :: INCSP_1:26
for S being IncSpace
for A being POINT of S
for L being LINE of S st not A on L holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
proof
let S be IncSpace; ::_thesis: for A being POINT of S
for L being LINE of S st not A on L holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
let A be POINT of S; ::_thesis: for L being LINE of S st not A on L holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
let L be LINE of S; ::_thesis: ( not A on L implies ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q ) )
assume A1: not A on L ; ::_thesis: ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
consider B, C being POINT of S such that
A2: B <> C and
A3: {B,C} on L by Def8;
consider P being PLANE of S such that
A4: {B,C,A} on P by Def12;
take  P ; ::_thesis: for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
let Q be PLANE of S; ::_thesis: ( ( A on Q & L on Q ) iff P = Q )
thus  ( A on Q & L on Q implies P = Q ) ::_thesis: ( P = Q implies ( A on Q & L on Q ) )
proof
assume that
A5: A on Q and
A6: L on Q ; ::_thesis: P = Q
 {B,C} on Q by A3, A6, Th14;
then  ( B on Q & C on Q ) by Th3;
then A7: {B,C,A} on Q by A5, Th4;
 not {B,C,A} is linear by A1, A2, A3, Th18;
hence  P = Q by A4, A7, Def13; ::_thesis: verum
end;
A8: {B,C} \/ {A} on P by A4, ENUMSET1:3;
thus  ( P = Q implies ( A on Q & L on Q ) ) by A2, A3, A8, Def14, Th9; ::_thesis: verum
end;

theorem Th27: :: INCSP_1:27
for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )
proof
let S be IncSpace; ::_thesis: for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )
let K, L be LINE of S; ::_thesis: ( K <> L & ex A being POINT of S st
( A on K & A on L ) implies ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q ) )
assume that
A1: K <> L and
A2: ex A being POINT of S st
( A on K & A on L ) ; ::_thesis: ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )
consider A being POINT of S such that
A3: A on K and
A4: A on L by A2;
consider C being POINT of S such that
A5: A <> C and
A6: C on L by Lm1;
consider B being POINT of S such that
A7: A <> B and
A8: B on K by Lm1;
consider P being PLANE of S such that
A9: {A,B,C} on P by Def12;
A10: A on P by A9, Th4;
take  P ; ::_thesis: for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )
let Q be PLANE of S; ::_thesis: ( ( K on Q & L on Q ) iff P = Q )
thus  ( K on Q & L on Q implies P = Q ) ::_thesis: ( P = Q implies ( K on Q & L on Q ) )
proof
 {A,C} on L by A4, A6, Th1;
then  not {A,C} on K by A1, A5, Def10;
then A11: not C on K by A3, Th1;
assume that
A12: K on Q and
A13: L on Q ; ::_thesis: P = Q
A14: C on Q by A6, A13, Def17;
 ( A on Q & B on Q ) by A3, A8, A12, Def17;
then A15: {A,B,C} on Q by A14, Th4;
 {A,B} on K by A3, A8, Th1;
then  not {A,B,C} is linear by A7, A11, Th18;
hence  P = Q by A9, A15, Def13; ::_thesis: verum
end;
 B on P by A9, Th4;
then A16: {A,B} on P by A10, Th3;
 C on P by A9, Th4;
then A17: {A,C} on P by A10, Th3;
A18: {A,C} on L by A4, A6, Th1;
 {A,B} on K by A3, A8, Th1;
hence  ( P = Q implies ( K on Q & L on Q ) ) by A7, A5, A18, A16, A17, Def14; ::_thesis: verum
end;

definition
let S be IncSpace;
let A, B be POINT of S;
assume A1: A <> B ;
func Line (A,B) ->  LINE of S means :Def19: :: INCSP_1:def 19
{A,B} on it;
correctness
existence
ex b1 being LINE of S st {A,B} on b1;
uniqueness
for b1, b2 being LINE of S st {A,B} on b1 & {A,B} on b2 holds
b1 = b2;
by A1, Def9, Def10;
end;

:: deftheorem Def19 defines Line INCSP_1:def_19_:_
 for S being IncSpace
for A, B being POINT of S st A <> B holds
for b4 being LINE of S holds
( b4 = Line (A,B) iff {A,B} on b4 );

definition
let S be IncSpace;
let A, B, C be POINT of S;
assume A1: not {A,B,C} is linear ;
func Plane (A,B,C) ->  PLANE of S means :Def20: :: INCSP_1:def 20
{A,B,C} on it;
correctness
existence
ex b1 being PLANE of S st {A,B,C} on b1;
uniqueness
for b1, b2 being PLANE of S st {A,B,C} on b1 & {A,B,C} on b2 holds
b1 = b2;
by A1, Def12, Def13;
end;

:: deftheorem Def20 defines Plane INCSP_1:def_20_:_
 for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
for b5 being PLANE of S holds
( b5 = Plane (A,B,C) iff {A,B,C} on b5 );

definition
let S be IncSpace;
let A be POINT of S;
let L be LINE of S;
assume A1: not A on L ;
func Plane (A,L) ->  PLANE of S means :Def21: :: INCSP_1:def 21
( A on it & L on it );
existence
 ex b1 being PLANE of S st
( A on b1 & L on b1 )
proof
consider B, C being POINT of S such that
A2: ( B <> C & {B,C} on L ) by Def8;
consider P being PLANE of S such that
A3: {B,C,A} on P by Def12;
take  P ; ::_thesis: ( A on P & L on P )
thus  A on P by A3, Th4; ::_thesis: L on P
 {B,C} \/ {A} on P by A3, ENUMSET1:3;
then  {B,C} on P by Th9;
hence  L on P by A2, Def14; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PLANE of S st A on b1 & L on b1 & A on b2 & L on b2 holds
b1 = b2
proof
let P, Q be PLANE of S; ::_thesis: ( A on P & L on P & A on Q & L on Q implies P = Q )
assume that
A4: ( A on P & L on P ) and
A5: ( A on Q & L on Q ) ; ::_thesis: P = Q
consider P1 being PLANE of S such that
A6: for P2 being PLANE of S holds
( ( A on P2 & L on P2 ) iff P1 = P2 ) by A1, Th26;
 P1 = P by A4, A6;
hence  P = Q by A5, A6; ::_thesis: verum
end;
end;

:: deftheorem Def21 defines Plane INCSP_1:def_21_:_
 for S being IncSpace
for A being POINT of S
for L being LINE of S st not A on L holds
for b4 being PLANE of S holds
( b4 = Plane (A,L) iff ( A on b4 & L on b4 ) );

definition
let S be IncSpace;
let K, L be LINE of S;
assume that
A1: K <> L and
A2: ex A being POINT of S st
( A on K & A on L ) ;
func Plane (K,L) ->  PLANE of S means :Def22: :: INCSP_1:def 22
( K on it & L on it );
existence
 ex b1 being PLANE of S st
( K on b1 & L on b1 ) by A2, Th23;
uniqueness
 for b1, b2 being PLANE of S st K on b1 & L on b1 & K on b2 & L on b2 holds
b1 = b2
proof
let P, Q be PLANE of S; ::_thesis: ( K on P & L on P & K on Q & L on Q implies P = Q )
assume that
A3: ( K on P & L on P ) and
A4: ( K on Q & L on Q ) ; ::_thesis: P = Q
consider P1 being PLANE of S such that
A5: for P2 being PLANE of S holds
( ( K on P2 & L on P2 ) iff P1 = P2 ) by A1, A2, Th27;
 P = P1 by A3, A5;
hence  P = Q by A4, A5; ::_thesis: verum
end;
end;

:: deftheorem Def22 defines Plane INCSP_1:def_22_:_
 for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
for b4 being PLANE of S holds
( b4 = Plane (K,L) iff ( K on b4 & L on b4 ) );

theorem :: INCSP_1:28
for S being IncSpace
for A, B being POINT of S st A <> B holds
Line (A,B) = Line (B,A)
proof
let S be IncSpace; ::_thesis: for A, B being POINT of S st A <> B holds
Line (A,B) = Line (B,A)
let A, B be POINT of S; ::_thesis: ( A <> B implies Line (A,B) = Line (B,A) )
assume A1: A <> B ; ::_thesis: Line (A,B) = Line (B,A)
then  {A,B} on Line (A,B) by Def19;
hence  Line (A,B) = Line (B,A) by A1, Def19; ::_thesis: verum
end;

theorem Th29: :: INCSP_1:29
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (A,C,B)
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (A,C,B)
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane (A,C,B) )
assume A1: not {A,B,C} is linear ; ::_thesis: Plane (A,B,C) = Plane (A,C,B)
then  not {A,C,B} is linear by ENUMSET1:57;
then  {A,C,B} on Plane (A,C,B) by Def20;
then  {A,B,C} on Plane (A,C,B) by ENUMSET1:57;
hence  Plane (A,B,C) = Plane (A,C,B) by A1, Def20; ::_thesis: verum
end;

theorem Th30: :: INCSP_1:30
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (B,A,C)
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (B,A,C)
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane (B,A,C) )
assume A1: not {A,B,C} is linear ; ::_thesis: Plane (A,B,C) = Plane (B,A,C)
then  not {B,A,C} is linear by ENUMSET1:58;
then  {B,A,C} on Plane (B,A,C) by Def20;
then  {A,B,C} on Plane (B,A,C) by ENUMSET1:58;
hence  Plane (A,B,C) = Plane (B,A,C) by A1, Def20; ::_thesis: verum
end;

theorem :: INCSP_1:31
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (B,C,A)
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (B,C,A)
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane (B,C,A) )
assume A1: not {A,B,C} is linear ; ::_thesis: Plane (A,B,C) = Plane (B,C,A)
then A2: not {B,C,A} is linear by ENUMSET1:59;
thus  Plane (A,B,C) = Plane (B,A,C) by A1, Th30
.= Plane (B,C,A) by A2, Th29 ; ::_thesis: verum
end;

theorem Th32: :: INCSP_1:32
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,A,B)
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,A,B)
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane (C,A,B) )
assume A1: not {A,B,C} is linear ; ::_thesis: Plane (A,B,C) = Plane (C,A,B)
then A2: not {C,A,B} is linear by ENUMSET1:59;
thus  Plane (A,B,C) = Plane (A,C,B) by A1, Th29
.= Plane (C,A,B) by A2, Th30 ; ::_thesis: verum
end;

theorem :: INCSP_1:33
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,B,A)
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,B,A)
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane (C,B,A) )
assume A1: not {A,B,C} is linear ; ::_thesis: Plane (A,B,C) = Plane (C,B,A)
then A2: not {C,B,A} is linear by ENUMSET1:60;
thus  Plane (A,B,C) = Plane (C,A,B) by A1, Th32
.= Plane (C,B,A) by A2, Th29 ; ::_thesis: verum
end;

theorem :: INCSP_1:34
for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
Plane (K,L) = Plane (L,K)
proof
let S be IncSpace; ::_thesis: for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
Plane (K,L) = Plane (L,K)
let K, L be LINE of S; ::_thesis: ( K <> L & ex A being POINT of S st
( A on K & A on L ) implies Plane (K,L) = Plane (L,K) )
assume A1: K <> L ; ::_thesis: ( for A being POINT of S holds
( not A on K or not A on L ) or Plane (K,L) = Plane (L,K) )
set P2 = Plane (L,K);
set P1 = Plane (K,L);
given A being POINT of S such that A2: A on K and
A3: A on L ; ::_thesis: Plane (K,L) = Plane (L,K)
consider C being POINT of S such that
A4: A <> C and
A5: C on L by Lm1;
consider B being POINT of S such that
A6: A <> B and
A7: B on K by Lm1;
A8: K on Plane (L,K) by A1, A2, A3, Def22;
then A9: B on Plane (L,K) by A7, Def17;
A10: K on Plane (K,L) by A1, A2, A3, Def22;
then A11: B on Plane (K,L) by A7, Def17;
A12: now__::_thesis:_not_{A,B,C}_is_linear
assume  {A,B,C} is linear ; ::_thesis: contradiction
then consider L1 being LINE of S such that
A13: {A,B,C} on L1 by Def6;
A14: A on L1 by A13, Th2;
 C on L1 by A13, Th2;
then A15: {A,C} on L1 by A14, Th1;
A16: {A,B} on K by A2, A7, Th1;
 B on L1 by A13, Th2;
then  {A,B} on L1 by A14, Th1;
then A17: K = L1 by A6, A16, Def10;
 {A,C} on L by A3, A5, Th1;
hence  contradiction by A1, A4, A15, A17, Def10; ::_thesis: verum
end;
 L on Plane (L,K) by A1, A2, A3, Def22;
then A18: C on Plane (L,K) by A5, Def17;
 A on Plane (L,K) by A2, A8, Def17;
then A19: {A,B,C} on Plane (L,K) by A9, A18, Th4;
 L on Plane (K,L) by A1, A2, A3, Def22;
then A20: C on Plane (K,L) by A5, Def17;
 A on Plane (K,L) by A2, A10, Def17;
then  {A,B,C} on Plane (K,L) by A11, A20, Th4;
hence  Plane (K,L) = Plane (L,K) by A19, A12, Def13; ::_thesis: verum
end;

theorem Th35: :: INCSP_1:35
for S being IncSpace
for A, B, C being POINT of S st A <> B & C on Line (A,B) holds
{A,B,C} is linear
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st A <> B & C on Line (A,B) holds
{A,B,C} is linear
let A, B, C be POINT of S; ::_thesis: ( A <> B & C on Line (A,B) implies {A,B,C} is linear )
assume  A <> B ; ::_thesis: ( not C on Line (A,B) or {A,B,C} is linear )
then  {A,B} on Line (A,B) by Def19;
then A1: ( A on Line (A,B) & B on Line (A,B) ) by Th1;
assume  C on Line (A,B) ; ::_thesis: {A,B,C} is linear
then  {A,B,C} on Line (A,B) by A1, Th2;
hence  {A,B,C} is linear by Def6; ::_thesis: verum
end;

theorem :: INCSP_1:36
for S being IncSpace
for A, B, C being POINT of S st A <> B & A <> C & {A,B,C} is linear holds
Line (A,B) = Line (A,C)
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st A <> B & A <> C & {A,B,C} is linear holds
Line (A,B) = Line (A,C)
let A, B, C be POINT of S; ::_thesis: ( A <> B & A <> C & {A,B,C} is linear implies Line (A,B) = Line (A,C) )
assume A1: A <> B ; ::_thesis: ( not A <> C or not {A,B,C} is linear or Line (A,B) = Line (A,C) )
then A2: {A,B} on Line (A,B) by Def19;
then A3: A on Line (A,B) by Th1;
assume A4: A <> C ; ::_thesis: ( not {A,B,C} is linear or Line (A,B) = Line (A,C) )
assume  {A,B,C} is linear ; ::_thesis: Line (A,B) = Line (A,C)
then  C on Line (A,B) by A1, A2, Th18;
then  {A,C} on Line (A,B) by A3, Th1;
hence  Line (A,B) = Line (A,C) by A4, Def19; ::_thesis: verum
end;

theorem :: INCSP_1:37
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,(Line (A,B)))
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,(Line (A,B)))
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane (C,(Line (A,B))) )
assume A1: not {A,B,C} is linear ; ::_thesis: Plane (A,B,C) = Plane (C,(Line (A,B)))
then  A <> B by Th15;
then A2: {A,B} on Line (A,B) by Def19;
then  ( A on Line (A,B) & B on Line (A,B) ) by Th1;
then A3: ( C on Line (A,B) implies {A,B,C} on Line (A,B) ) by Th2;
then  Line (A,B) on Plane (C,(Line (A,B))) by A1, Def6, Def21;
then A4: {A,B} on Plane (C,(Line (A,B))) by A2, Th14;
 C on Plane (C,(Line (A,B))) by A1, A3, Def6, Def21;
then  {A,B} \/ {C} on Plane (C,(Line (A,B))) by A4, Th9;
then  {A,B,C} on Plane (C,(Line (A,B))) by ENUMSET1:3;
hence  Plane (A,B,C) = Plane (C,(Line (A,B))) by A1, Def20; ::_thesis: verum
end;

theorem :: INCSP_1:38
for S being IncSpace
for A, B, C, D being POINT of S st not {A,B,C} is linear & D on Plane (A,B,C) holds
{A,B,C,D} is planar
proof
let S be IncSpace; ::_thesis: for A, B, C, D being POINT of S st not {A,B,C} is linear & D on Plane (A,B,C) holds
{A,B,C,D} is planar
let A, B, C, D be POINT of S; ::_thesis: ( not {A,B,C} is linear & D on Plane (A,B,C) implies {A,B,C,D} is planar )
assume that
A1: not {A,B,C} is linear and
A2: D on Plane (A,B,C) ; ::_thesis: {A,B,C,D} is planar
 {A,B,C} on Plane (A,B,C) by A1, Def20;
then  {A,B,C} \/ {D} on Plane (A,B,C) by A2, Th9;
then  {A,B,C,D} on Plane (A,B,C) by ENUMSET1:6;
hence  {A,B,C,D} is planar by Def7; ::_thesis: verum
end;

theorem :: INCSP_1:39
for S being IncSpace
for C, A, B being POINT of S
for L being LINE of S st not C on L & {A,B} on L & A <> B holds
Plane (C,L) = Plane (A,B,C)
proof
let S be IncSpace; ::_thesis: for C, A, B being POINT of S
for L being LINE of S st not C on L & {A,B} on L & A <> B holds
Plane (C,L) = Plane (A,B,C)
let C, A, B be POINT of S; ::_thesis: for L being LINE of S st not C on L & {A,B} on L & A <> B holds
Plane (C,L) = Plane (A,B,C)
let L be LINE of S; ::_thesis: ( not C on L & {A,B} on L & A <> B implies Plane (C,L) = Plane (A,B,C) )
assume that
A1: not C on L and
A2: {A,B} on L and
A3: A <> B ; ::_thesis: Plane (C,L) = Plane (A,B,C)
set P1 = Plane (C,L);
 L on Plane (C,L) by A1, Def21;
then A4: {A,B} on Plane (C,L) by A2, Th14;
 C on Plane (C,L) by A1, Def21;
then  {A,B} \/ {C} on Plane (C,L) by A4, Th9;
then A5: {A,B,C} on Plane (C,L) by ENUMSET1:3;
 not {A,B,C} is linear by A1, A2, A3, Th18;
hence  Plane (C,L) = Plane (A,B,C) by A5, Def20; ::_thesis: verum
end;

theorem :: INCSP_1:40
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C)))
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C)))
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C))) )
set P2 = Plane ((Line (A,B)),(Line (A,C)));
set L1 = Line (A,B);
set L2 = Line (A,C);
assume A1: not {A,B,C} is linear ; ::_thesis: Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C)))
then A2: A <> B by Th15;
then A3: {A,B} on Line (A,B) by Def19;
then A4: A on Line (A,B) by Th1;
 not {A,C,B} is linear by A1, ENUMSET1:57;
then A5: A <> C by Th15;
then A6: {A,C} on Line (A,C) by Def19;
then A7: A on Line (A,C) by Th1;
 {A,C} on Line (A,C) by A5, Def19;
then  C on Line (A,C) by Th1;
then A8: Line (A,B) <> Line (A,C) by A1, A2, Th35;
then  Line (A,C) on Plane ((Line (A,B)),(Line (A,C))) by A4, A7, Def22;
then  {A,C} on Plane ((Line (A,B)),(Line (A,C))) by A6, Th14;
then A9: C on Plane ((Line (A,B)),(Line (A,C))) by Th3;
 Line (A,B) on Plane ((Line (A,B)),(Line (A,C))) by A4, A7, A8, Def22;
then  {A,B} on Plane ((Line (A,B)),(Line (A,C))) by A3, Th14;
then  {A,B} \/ {C} on Plane ((Line (A,B)),(Line (A,C))) by A9, Th9;
then  {A,B,C} on Plane ((Line (A,B)),(Line (A,C))) by ENUMSET1:3;
hence  Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C))) by A1, Def20; ::_thesis: verum
end;

Lm2:  for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
proof
let S be IncSpace; ::_thesis: for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
let P be PLANE of S; ::_thesis: ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
consider A being POINT of S such that
A1: A on P by Def11;
consider A1, B1, C1, D1 being POINT of S such that
A2: not {A1,B1,C1,D1} is planar by Def16;
now__::_thesis:_(_not_A1_on_P_implies_ex_A,_B,_C,_D_being_POINT_of_S_st_
(_A_on_P_&_not_{A,B,C,D}_is_planar_)_)
assume A3: not A1 on P ; ::_thesis: ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
A4: now__::_thesis:_(_A_on_Line_(A1,B1)_implies_ex_A,_B,_C,_D_being_POINT_of_S_st_
(_A_on_P_&_not_{A,B,C,D}_is_planar_)_)
A5: A1 <> B1 by A2, Th16;
then A6: {A1,B1} on Line (A1,B1) by Def19;
 {A1,B1} on Line (A1,B1) by A5, Def19;
then  ( C1 on Line (A1,B1) implies {A1,B1} \/ {C1} on Line (A1,B1) ) by Th8;
then A7: ( C1 on Line (A1,B1) implies {A1,B1,C1} on Line (A1,B1) ) by ENUMSET1:3;
set Q = Plane (A1,B1,C1);
assume A8: A on Line (A1,B1) ; ::_thesis: ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
A9: not {A1,B1,C1} is linear by A2, Th17;
then  {A1,B1,C1} on Plane (A1,B1,C1) by Def20;
then A10: ( A1 on Plane (A1,B1,C1) & C1 on Plane (A1,B1,C1) ) by Th4;
A11: {A1,B1,C1} on Plane (A1,B1,C1) by A9, Def20;
then  ( D1 on Plane (A1,B1,C1) implies {A1,B1,C1} \/ {D1} on Plane (A1,B1,C1) ) by Th9;
then A12: ( D1 on Plane (A1,B1,C1) implies {A1,B1,C1,D1} on Plane (A1,B1,C1) ) by ENUMSET1:6;
 {A1,B1} \/ {C1} on Plane (A1,B1,C1) by A11, ENUMSET1:3;
then  {A1,B1} on Plane (A1,B1,C1) by Th11;
then  Line (A1,B1) on Plane (A1,B1,C1) by A5, A6, Def14;
then  A on Plane (A1,B1,C1) by A8, Def17;
then A13: {A,A1,C1} on Plane (A1,B1,C1) by A10, Th4;
 A1 on Line (A1,B1) by A6, Th1;
then  {A,A1} on Line (A1,B1) by A8, Th1;
then  not {A,A1,C1} is linear by A1, A3, A9, A7, Def6, Th18;
then  not {A,A1,C1,D1} is planar by A2, A12, A13, Def7, Th19;
hence  ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by A1; ::_thesis: verum
end;
now__::_thesis:_(_not_A_on_Line_(A1,B1)_implies_ex_A,_B,_C,_D_being_POINT_of_S_st_
(_A_on_P_&_not_{A,B,C,D}_is_planar_)_)
set Q = Plane (A1,B1,A);
assume A14: not A on Line (A1,B1) ; ::_thesis: ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
A15: A1 <> B1 by A2, Th16;
then A16: {A1,B1} on Line (A1,B1) by Def19;
then  not {A1,B1,A} is linear by A14, A15, Th18;
then A17: {A1,B1,A} on Plane (A1,B1,A) by Def20;
then  {A1,B1} \/ {A} on Plane (A1,B1,A) by ENUMSET1:3;
then  {A1,B1} on Plane (A1,B1,A) by Th9;
then  ( {C1,D1} on Plane (A1,B1,A) implies {A1,B1} \/ {C1,D1} on Plane (A1,B1,A) ) by Th11;
then  ( {C1,D1} on Plane (A1,B1,A) implies {A1,B1,C1,D1} on Plane (A1,B1,A) ) by ENUMSET1:5;
then  ( not C1 on Plane (A1,B1,A) or not D1 on Plane (A1,B1,A) ) by A2, Def7, Th3;
then  ( not {A1,B1,A,C1} is planar or not {A1,B1,A,D1} is planar ) by A14, A15, A16, A17, Th18, Th19;
then  ( not {A,A1,B1,C1} is planar or not {A,A1,B1,D1} is planar ) by ENUMSET1:67;
hence  ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by A1; ::_thesis: verum
end;
hence  ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by A4; ::_thesis: verum
end;
hence  ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by A2; ::_thesis: verum
end;

theorem Th41: :: INCSP_1:41
for S being IncSpace
for P being PLANE of S ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )
proof
let S be IncSpace; ::_thesis: for P being PLANE of S ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )
let P be PLANE of S; ::_thesis: ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )
consider A1, B1, C1, D1 being POINT of S such that
A1: A1 on P and
A2: not {A1,B1,C1,D1} is planar by Lm2;
 not {B1,D1,A1,C1} is planar by A2, ENUMSET1:69;
then A3: B1 <> D1 by Th16;
 not {C1,D1,A1,B1} is planar by A2, ENUMSET1:73;
then A4: C1 <> D1 by Th16;
 not {A1,B1,C1,D1} on P by A2, Def7;
then  not {B1,C1,D1,A1} on P by ENUMSET1:68;
then  not {B1,C1,D1} \/ {A1} on P by ENUMSET1:6;
then  not {B1,C1,D1} on P by A1, Th9;
then  ( not B1 on P or not C1 on P or not D1 on P ) by Th4;
then consider X being POINT of S such that
A5: ( X = B1 or X = C1 or X = D1 ) and
A6: not X on P ;
 not {B1,C1,A1,D1} is planar by A2, ENUMSET1:67;
then  B1 <> C1 by Th16;
then consider Y, Z being POINT of S such that
A7: ( ( Y = B1 or Y = C1 or Y = D1 ) & ( Z = B1 or Z = C1 or Z = D1 ) & Y <> X & Z <> X & Y <> Z ) by A5, A3, A4;
set P1 = Plane (X,Y,A1);
set P2 = Plane (X,Z,A1);
A8: now__::_thesis:_not_{A1,X,Y,Z}_is_planar
assume  {A1,X,Y,Z} is planar ; ::_thesis: contradiction
then  ( {A1,D1,B1,C1} is planar or {A1,D1,C1,B1} is planar ) by A2, A5, A7, ENUMSET1:62;
hence  contradiction by A2, ENUMSET1:63, ENUMSET1:64; ::_thesis: verum
end;
then  not {A1,X,Y} is linear by Th17;
then  not {X,Y,A1} is linear by ENUMSET1:59;
then A9: {X,Y,A1} on Plane (X,Y,A1) by Def20;
then A10: A1 on Plane (X,Y,A1) by Th4;
then consider B being POINT of S such that
A11: A1 <> B and
A12: B on Plane (X,Y,A1) and
A13: B on P by A1, Def15;
 not {X,Z,A1,Y} is planar by A8, ENUMSET1:69;
then  not {X,Z,A1} is linear by Th17;
then A14: {X,Z,A1} on Plane (X,Z,A1) by Def20;
then A15: A1 on Plane (X,Z,A1) by Th4;
then consider C being POINT of S such that
A16: A1 <> C and
A17: C on P and
A18: C on Plane (X,Z,A1) by A1, Def15;
take  A1 ; ::_thesis: ex B, C being POINT of S st
( {A1,B,C} on P & not {A1,B,C} is linear )
take  B ; ::_thesis: ex C being POINT of S st
( {A1,B,C} on P & not {A1,B,C} is linear )
take  C ; ::_thesis: ( {A1,B,C} on P & not {A1,B,C} is linear )
thus  {A1,B,C} on P by A1, A13, A17, Th4; ::_thesis: not {A1,B,C} is linear
given K being LINE of S such that A19: {A1,B,C} on K ; :: according to INCSP_1:def_6 ::_thesis: contradiction
A20: {A1,C} on Plane (X,Z,A1) by A15, A18, Th3;
 {A1,C,B} on K by A19, ENUMSET1:57;
then  {A1,C} \/ {B} on K by ENUMSET1:3;
then  {A1,C} on K by Th10;
then A21: K on Plane (X,Z,A1) by A16, A20, Def14;
consider E being POINT of S such that
A22: B <> E and
A23: E on K by Lm1;
 {A1,B} \/ {C} on K by A19, ENUMSET1:3;
then A24: {A1,B} on K by Th10;
A25: now__::_thesis:_not_{X,B,E}_is_linear
 {A1,B} on P by A1, A13, Th3;
then  K on P by A11, A24, Def14;
then  E on P by A23, Def17;
then A26: {E,B} on P by A13, Th3;
assume  {X,B,E} is linear ; ::_thesis: contradiction
then consider L being LINE of S such that
A27: {X,B,E} on L by Def6;
A28: X on L by A27, Th2;
 {E,B,X} on L by A27, ENUMSET1:60;
then  {E,B} \/ {X} on L by ENUMSET1:3;
then  {E,B} on L by Th8;
then  L on P by A22, A26, Def14;
hence  contradiction by A6, A28, Def17; ::_thesis: verum
end;
 B on K by A19, Th2;
then A29: B on Plane (X,Z,A1) by A21, Def17;
A30: X on Plane (X,Z,A1) by A14, Th4;
A31: X on Plane (X,Y,A1) by A9, Th4;
 {A1,B} on Plane (X,Y,A1) by A10, A12, Th3;
then  K on Plane (X,Y,A1) by A11, A24, Def14;
then  E on Plane (X,Y,A1) by A23, Def17;
then A32: {X,B,E} on Plane (X,Y,A1) by A12, A31, Th4;
 E on Plane (X,Z,A1) by A23, A21, Def17;
then  {X,B,E} on Plane (X,Z,A1) by A29, A30, Th4;
then  Plane (X,Y,A1) = Plane (X,Z,A1) by A25, A32, Def13;
then  Z on Plane (X,Y,A1) by A14, Th4;
then  {X,Y,A1} \/ {Z} on Plane (X,Y,A1) by A9, Th9;
then  {X,Y,A1,Z} on Plane (X,Y,A1) by ENUMSET1:6;
then  {X,Y,A1,Z} is planar by Def7;
hence  contradiction by A8, ENUMSET1:67; ::_thesis: verum
end;

theorem :: INCSP_1:42
for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by Lm2;

theorem :: INCSP_1:43
for S being IncSpace
for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L ) by Lm1;

theorem Th44: :: INCSP_1:44
for S being IncSpace
for A, B being POINT of S
for P being PLANE of S st A <> B holds
ex C being POINT of S st
( C on P & not {A,B,C} is linear )
proof
let S be IncSpace; ::_thesis: for A, B being POINT of S
for P being PLANE of S st A <> B holds
ex C being POINT of S st
( C on P & not {A,B,C} is linear )
let A, B be POINT of S; ::_thesis: for P being PLANE of S st A <> B holds
ex C being POINT of S st
( C on P & not {A,B,C} is linear )
let P be PLANE of S; ::_thesis: ( A <> B implies ex C being POINT of S st
( C on P & not {A,B,C} is linear ) )
consider L being LINE of S such that
A1: {A,B} on L by Def9;
consider C, D, E being POINT of S such that
A2: {C,D,E} on P and
A3: not {C,D,E} is linear by Th41;
A4: ( C on P & D on P ) by A2, Th4;
 not {C,D,E} on L by A3, Def6;
then A5: ( not C on L or not D on L or not E on L ) by Th2;
A6: E on P by A2, Th4;
assume  A <> B ; ::_thesis: ex C being POINT of S st
( C on P & not {A,B,C} is linear )
then  ( not {A,B,C} is linear or not {A,B,D} is linear or not {A,B,E} is linear ) by A1, A5, Th18;
hence  ex C being POINT of S st
( C on P & not {A,B,C} is linear ) by A4, A6; ::_thesis: verum
end;

theorem Th45: :: INCSP_1:45
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
ex D being POINT of S st not {A,B,C,D} is planar
proof
let S be IncSpace; ::_thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
ex D being POINT of S st not {A,B,C,D} is planar
let A, B, C be POINT of S; ::_thesis: ( not {A,B,C} is linear implies ex D being POINT of S st not {A,B,C,D} is planar )
assume A1: not {A,B,C} is linear ; ::_thesis: not for D being POINT of S holds {A,B,C,D} is planar
consider P being PLANE of S such that
A2: {A,B,C} on P by Def12;
consider A1, B1, C1, D1 being POINT of S such that
A3: not {A1,B1,C1,D1} is planar by Def16;
 not {A1,B1,C1,D1} on P by A3, Def7;
then  ( not A1 on P or not B1 on P or not C1 on P or not D1 on P ) by Th5;
then  ( not {A,B,C,A1} is planar or not {A,B,C,B1} is planar or not {A,B,C,C1} is planar or not {A,B,C,D1} is planar ) by A1, A2, Th19;
hence  not for D being POINT of S holds {A,B,C,D} is planar ; ::_thesis: verum
end;

theorem Th46: :: INCSP_1:46
for S being IncSpace
for A being POINT of S
for P being PLANE of S ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
proof
let S be IncSpace; ::_thesis: for A being POINT of S
for P being PLANE of S ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
let A be POINT of S; ::_thesis: for P being PLANE of S ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
let P be PLANE of S; ::_thesis: ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
A1: now__::_thesis:_(_not_A_on_P_implies_ex_B,_C_being_POINT_of_S_st_
(_{B,C}_on_P_&_not_{A,B,C}_is_linear_)_)
assume A2: not A on P ; ::_thesis: ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
consider B, C, D being POINT of S such that
A3: {B,C,D} on P and
A4: not {B,C,D} is linear by Th41;
A5: B <> C by A4, Th15;
take B = B; ::_thesis: ex C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
take C = C; ::_thesis: ( {B,C} on P & not {A,B,C} is linear )
 {B,C} \/ {D} on P by A3, ENUMSET1:3;
hence A6: {B,C} on P by Th9; ::_thesis: not {A,B,C} is linear
assume  {A,B,C} is linear ; ::_thesis: contradiction
then consider K being LINE of S such that
A7: {A,B,C} on K by Def6;
 {B,C,A} on K by A7, ENUMSET1:59;
then A8: {B,C} \/ {A} on K by ENUMSET1:3;
then A9: A on K by Th8;
 {B,C} on K by A8, Th10;
then  K on P by A6, A5, Def14;
hence  contradiction by A2, A9, Def17; ::_thesis: verum
end;
now__::_thesis:_(_A_on_P_implies_ex_B,_C_being_POINT_of_S_st_
(_{B,C}_on_P_&_not_{A,B,C}_is_linear_)_)
assume  A on P ; ::_thesis: ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
then consider B being POINT of S such that
A10: A <> B and
A11: B on P and
 B on P by Def15;
consider C being POINT of S such that
A12: C on P and
A13: not {A,B,C} is linear by A10, Th44;
 {B,C} on P by A11, A12, Th3;
hence  ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear ) by A13; ::_thesis: verum
end;
hence  ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear ) by A1; ::_thesis: verum
end;

theorem Th47: :: INCSP_1:47
for S being IncSpace
for A, B being POINT of S st A <> B holds
ex C, D being POINT of S st not {A,B,C,D} is planar
proof
let S be IncSpace; ::_thesis: for A, B being POINT of S st A <> B holds
ex C, D being POINT of S st not {A,B,C,D} is planar
let A, B be POINT of S; ::_thesis: ( A <> B implies ex C, D being POINT of S st not {A,B,C,D} is planar )
set P = the PLANE of S;
assume  A <> B ; ::_thesis: not for C, D being POINT of S holds {A,B,C,D} is planar
then consider C being POINT of S such that
 C on the PLANE of S and
A1: not {A,B,C} is linear by Th44;
 not for D being POINT of S holds {A,B,C,D} is planar by A1, Th45;
hence  not for C, D being POINT of S holds {A,B,C,D} is planar ; ::_thesis: verum
end;

theorem :: INCSP_1:48
for S being IncSpace
for A being POINT of S holds
not for B, C, D being POINT of S holds {A,B,C,D} is planar
proof
let S be IncSpace; ::_thesis: for A being POINT of S holds
not for B, C, D being POINT of S holds {A,B,C,D} is planar
let A be POINT of S; ::_thesis: not for B, C, D being POINT of S holds {A,B,C,D} is planar
set L = the LINE of S;
consider B being POINT of S such that
A1: A <> B and
 B on the LINE of S by Lm1;
 not for C, D being POINT of S holds {A,B,C,D} is planar by A1, Th47;
hence  not for B, C, D being POINT of S holds {A,B,C,D} is planar ; ::_thesis: verum
end;

theorem :: INCSP_1:49
for S being IncSpace
for A being POINT of S
for P being PLANE of S ex L being LINE of S st
( not A on L & L on P )
proof
let S be IncSpace; ::_thesis: for A being POINT of S
for P being PLANE of S ex L being LINE of S st
( not A on L & L on P )
let A be POINT of S; ::_thesis: for P being PLANE of S ex L being LINE of S st
( not A on L & L on P )
let P be PLANE of S; ::_thesis: ex L being LINE of S st
( not A on L & L on P )
consider B, C being POINT of S such that
A1: {B,C} on P and
A2: not {A,B,C} is linear by Th46;
consider L being LINE of S such that
A3: {B,C} on L by Def9;
take  L ; ::_thesis: ( not A on L & L on P )
 ( A on L implies {B,C} \/ {A} on L ) by A3, Th8;
then  ( A on L implies {B,C,A} on L ) by ENUMSET1:3;
then  ( A on L implies {A,B,C} on L ) by ENUMSET1:59;
hence  not A on L by A2, Def6; ::_thesis: L on P
 not {B,C,A} is linear by A2, ENUMSET1:59;
then  B <> C by Th15;
hence  L on P by A1, A3, Def14; ::_thesis: verum
end;

theorem Th50: :: INCSP_1:50
for S being IncSpace
for A being POINT of S
for P being PLANE of S st A on P holds
ex L, L1, L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )
proof
let S be IncSpace; ::_thesis: for A being POINT of S
for P being PLANE of S st A on P holds
ex L, L1, L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )
let A be POINT of S; ::_thesis: for P being PLANE of S st A on P holds
ex L, L1, L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )
let P be PLANE of S; ::_thesis: ( A on P implies ex L, L1, L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 ) )
consider B, C being POINT of S such that
A1: {B,C} on P and
A2: not {A,B,C} is linear by Th46;
consider D being POINT of S such that
A3: not {A,B,C,D} is planar by A2, Th45;
assume  A on P ; ::_thesis: ex L, L1, L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )
then A4: {A} \/ {B,C} on P by A1, Th9;
then A5: {A,B,C} on P by ENUMSET1:2;
take L3 = Line (A,D); ::_thesis: ex L1, L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )
take L1 = Line (A,B); ::_thesis: ex L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )
take L2 = Line (A,C); ::_thesis: ( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )
A6: A <> B by A2, Th15;
then A7: {A,B} on L1 by Def19;
A8: not {A,C,B} is linear by A2, ENUMSET1:57;
then A9: A <> C by Th15;
then A10: {A,C} on L2 by Def19;
then  ( B on L2 implies {A,C} \/ {B} on L2 ) by Th8;
then  ( B on L2 implies {A,C,B} on L2 ) by ENUMSET1:3;
hence  L1 <> L2 by A8, A7, Def6, Th1; ::_thesis: ( L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )
 {A,B} \/ {C} on P by A5, ENUMSET1:3;
then  {A,B} on P by Th11;
hence  L1 on P by A6, A7, Def14; ::_thesis: ( L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )
 {A,C,B} on P by A4, ENUMSET1:2;
then  {A,C} \/ {B} on P by ENUMSET1:3;
then  {A,C} on P by Th9;
hence  L2 on P by A9, A10, Def14; ::_thesis: ( not L3 on P & A on L3 & A on L1 & A on L2 )
 not {A,D,B,C} is planar by A3, ENUMSET1:63;
then  A <> D by Th16;
then A11: {A,D} on L3 by Def19;
then  ( L3 on P implies {A,D} on P ) by Th14;
then  ( L3 on P implies D on P ) by Th3;
then  ( L3 on P implies {A,B,C} \/ {D} on P ) by A5, Th9;
then  ( L3 on P implies {A,B,C,D} on P ) by ENUMSET1:6;
hence  not L3 on P by A3, Def7; ::_thesis: ( A on L3 & A on L1 & A on L2 )
thus  ( A on L3 & A on L1 & A on L2 ) by A10, A7, A11, Th1; ::_thesis: verum
end;

theorem :: INCSP_1:51
for S being IncSpace
for A being POINT of S ex L, L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
proof
let S be IncSpace; ::_thesis: for A being POINT of S ex L, L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
let A be POINT of S; ::_thesis: ex L, L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
consider P being PLANE of S such that
A1: {A,A,A} on P by Def12;
 A on P by A1, Th4;
then consider L, L1, L2 being LINE of S such that
A2: L1 <> L2 and
A3: L1 on P and
A4: L2 on P and
A5: not L on P and
A6: A on L and
A7: A on L1 and
A8: A on L2 by Th50;
consider B being POINT of S such that
A9: A <> B and
A10: B on L1 by Lm1;
consider C being POINT of S such that
A11: A <> C and
A12: C on L2 by Lm1;
A13: C on P by A4, A12, Def17;
A14: {A,B} on L1 by A7, A10, Th1;
then  {A,B} on P by A3, Th14;
then  {A,B} \/ {C} on P by A13, Th9;
then A15: {A,B,C} on P by ENUMSET1:3;
take  L ; ::_thesis: ex L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
take  L1 ; ::_thesis: ex L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
take  L2 ; ::_thesis: ( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
thus  ( A on L & A on L1 & A on L2 ) by A6, A7, A8; ::_thesis: for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P )
given Q being PLANE of S such that A16: L on Q and
A17: L1 on Q and
A18: L2 on Q ; ::_thesis: contradiction
A19: C on Q by A18, A12, Def17;
A20: {A,C} on L2 by A8, A12, Th1;
now__::_thesis:_for_K_being_LINE_of_S_holds_not_{A,B,C}_on_K
given K being LINE of S such that A21: {A,B,C} on K ; ::_thesis: contradiction
 {A,C,B} on K by A21, ENUMSET1:57;
then  {A,C} \/ {B} on K by ENUMSET1:3;
then A22: {A,C} on K by Th8;
 {A,B} \/ {C} on K by A21, ENUMSET1:3;
then  {A,B} on K by Th8;
then  K = L1 by A9, A14, Def10;
hence  contradiction by A2, A11, A20, A22, Def10; ::_thesis: verum
end;
then A23: not {A,B,C} is linear by Def6;
 {A,B} on Q by A17, A14, Th14;
then  {A,B} \/ {C} on Q by A19, Th9;
then  {A,B,C} on Q by ENUMSET1:3;
hence  contradiction by A5, A16, A15, A23, Def13; ::_thesis: verum
end;

theorem :: INCSP_1:52
for S being IncSpace
for A being POINT of S
for L being LINE of S ex P being PLANE of S st
( A on P & not L on P )
proof
let S be IncSpace; ::_thesis: for A being POINT of S
for L being LINE of S ex P being PLANE of S st
( A on P & not L on P )
let A be POINT of S; ::_thesis: for L being LINE of S ex P being PLANE of S st
( A on P & not L on P )
let L be LINE of S; ::_thesis: ex P being PLANE of S st
( A on P & not L on P )
consider B being POINT of S such that
A1: A <> B and
A2: B on L by Lm1;
consider C, D being POINT of S such that
A3: not {A,B,C,D} is planar by A1, Th47;
take P = Plane (A,C,D); ::_thesis: ( A on P & not L on P )
A4: not {A,C,D,B} is planar by A3, ENUMSET1:63;
then  not {A,C,D} is linear by Th17;
then A5: {A,C,D} on P by Def20;
hence  A on P by Th4; ::_thesis: not L on P
 ( B on P implies {A,C,D} \/ {B} on P ) by A5, Th9;
then  ( B on P implies {A,C,D,B} on P ) by ENUMSET1:6;
hence  not L on P by A2, A4, Def7, Def17; ::_thesis: verum
end;

theorem :: INCSP_1:53
for S being IncSpace
for L being LINE of S
for P being PLANE of S ex A being POINT of S st
( A on P & not A on L )
proof
let S be IncSpace; ::_thesis: for L being LINE of S
for P being PLANE of S ex A being POINT of S st
( A on P & not A on L )
let L be LINE of S; ::_thesis: for P being PLANE of S ex A being POINT of S st
( A on P & not A on L )
let P be PLANE of S; ::_thesis: ex A being POINT of S st
( A on P & not A on L )
consider A, B being POINT of S such that
A1: A <> B and
A2: {A,B} on L by Def8;
consider C being POINT of S such that
A3: C on P and
A4: not {A,B,C} is linear by A1, Th44;
take  C ; ::_thesis: ( C on P & not C on L )
thus  C on P by A3; ::_thesis: not C on L
 ( C on L implies {A,B} \/ {C} on L ) by A2, Th8;
then  ( C on L implies {A,B,C} on L ) by ENUMSET1:3;
hence  not C on L by A4, Def6; ::_thesis: verum
end;

theorem :: INCSP_1:54
for S being IncSpace
for L being LINE of S ex K being LINE of S st
for P being PLANE of S holds
( not L on P or not K on P )
proof
let S be IncSpace; ::_thesis: for L being LINE of S ex K being LINE of S st
for P being PLANE of S holds
( not L on P or not K on P )
let L be LINE of S; ::_thesis: ex K being LINE of S st
for P being PLANE of S holds
( not L on P or not K on P )
consider A, B being POINT of S such that
A1: A <> B and
A2: {A,B} on L by Def8;
consider C, D being POINT of S such that
A3: not {A,B,C,D} is planar by A1, Th47;
take K = Line (C,D); ::_thesis: for P being PLANE of S holds
( not L on P or not K on P )
given P being PLANE of S such that A4: L on P and
A5: K on P ; ::_thesis: contradiction
 not {C,D,A,B} is planar by A3, ENUMSET1:73;
then  C <> D by Th16;
then  {C,D} on K by Def19;
then A6: {C,D} on P by A5, Th14;
 {A,B} on P by A2, A4, Th14;
then  {A,B} \/ {C,D} on P by A6, Th11;
then  {A,B,C,D} on P by ENUMSET1:5;
hence  contradiction by A3, Def7; ::_thesis: verum
end;

theorem :: INCSP_1:55
for S being IncSpace
for L being LINE of S ex P, Q being PLANE of S st
( P <> Q & L on P & L on Q )
proof
let S be IncSpace; ::_thesis: for L being LINE of S ex P, Q being PLANE of S st
( P <> Q & L on P & L on Q )
let L be LINE of S; ::_thesis: ex P, Q being PLANE of S st
( P <> Q & L on P & L on Q )
consider A, B being POINT of S such that
A1: A <> B and
A2: {A,B} on L by Def8;
consider C, D being POINT of S such that
A3: not {A,B,C,D} is planar by A1, Th47;
take P = Plane (A,B,C); ::_thesis: ex Q being PLANE of S st
( P <> Q & L on P & L on Q )
take Q = Plane (A,B,D); ::_thesis: ( P <> Q & L on P & L on Q )
 not {A,B,C} is linear by A3, Th17;
then A4: {A,B,C} on P by Def20;
 not {A,B,D,C} is planar by A3, ENUMSET1:61;
then  not {A,B,D} is linear by Th17;
then A5: {A,B,D} on Q by Def20;
then  {A,B} \/ {D} on Q by ENUMSET1:3;
then A6: {A,B} on Q by Th11;
 D on Q by A5, Th4;
then  ( P = Q implies {A,B,C} \/ {D} on P ) by A4, Th9;
then  ( P = Q implies {A,B,C,D} on P ) by ENUMSET1:6;
hence  P <> Q by A3, Def7; ::_thesis: ( L on P & L on Q )
 {A,B} \/ {C} on P by A4, ENUMSET1:3;
then  {A,B} on P by Th11;
hence  ( L on P & L on Q ) by A1, A2, A6, Def14; ::_thesis: verum
end;

theorem :: INCSP_1:56
for S being IncSpace
for A, B being POINT of S
for L being LINE of S
for P being PLANE of S st not L on P & {A,B} on L & {A,B} on P holds
A = B by Def14;

theorem :: INCSP_1:57
for S being IncSpace
for P, Q being PLANE of S holds
( not P <> Q or for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )
proof
let S be IncSpace; ::_thesis: for P, Q being PLANE of S holds
( not P <> Q or for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )
let P, Q be PLANE of S; ::_thesis: ( not P <> Q or for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )
assume A1: P <> Q ; ::_thesis: ( for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )
given A being POINT of S such that A2: A on P and
A3: A on Q ; ::_thesis: ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L )
consider C being POINT of S such that
A4: A <> C and
A5: C on P and
A6: C on Q by A2, A3, Def15;
take L = Line (A,C); ::_thesis: for B being POINT of S holds
( ( B on P & B on Q ) iff B on L )
A7: {A,C} on L by A4, Def19;
 {A,C} on Q by A3, A6, Th3;
then A8: L on Q by A4, A7, Def14;
let B be POINT of S; ::_thesis: ( ( B on P & B on Q ) iff B on L )
 {A,C} on P by A2, A5, Th3;
then A9: L on P by A4, A7, Def14;
thus  ( B on P & B on Q implies B on L ) ::_thesis: ( B on L implies ( B on P & B on Q ) )
proof
assume that
A10: B on P and
A11: B on Q and
A12: not B on L ; ::_thesis: contradiction
consider P1 being PLANE of S such that
A13: for P2 being PLANE of S holds
( ( B on P2 & L on P2 ) iff P1 = P2 ) by A12, Th26;
 P = P1 by A9, A10, A13;
hence  contradiction by A1, A8, A11, A13; ::_thesis: verum
end;
thus  ( B on L implies ( B on P & B on Q ) ) by A9, A8, Def17; ::_thesis: verum
end;