:: Axioms of Incidence
::  by Wojciech A. Trybulec
::
:: Received April 14, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, RELAT_1, SUBSET_1, FDIFF_1, TARSKI, CARD_1, ZFMISC_1,
      INCSP_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1,
      ORDINAL1;
 constructors RELSET_1, DOMAIN_1, ORDINAL1;
 registrations XBOOLE_0, SUBSET_1;
 requirements SUBSET, BOOLE, NUMERALS;


begin

definition
  struct IncProjStr (# Points, Lines -> non empty set, Inc -> Relation of the
    Points, the Lines #);
end;

definition
  struct (IncProjStr) IncStruct (# Points, Lines, Planes -> non empty set, Inc
-> Relation of the Points,the Lines, Inc2 -> Relation of the Points,the Planes,
    Inc3 -> Relation of the Lines,the Planes #);
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;

reserve S for IncStruct;
reserve A,B,C,D for POINT of S;
reserve L for LINE of S;
reserve P for PLANE of S;
reserve F,G for Subset of the Points of S;

:: Definitions of predicates 'on' and attributes 'linear', 'planar'

definition
  let S be IncProjStr;
  let A be POINT of S, L be LINE of S;
  pred A on L means
:: INCSP_1:def 1

  [A,L] in the Inc of S;
end;

definition
  let S;
  let A be POINT of S, P be PLANE of S;
  pred A on P means
:: INCSP_1:def 2

  [A,P] in the Inc2 of S;
end;

definition
  let S;
  let L be LINE of S, P be PLANE of S;
  pred L on P means
:: INCSP_1:def 3

  [L,P] in the Inc3 of S;
end;

definition
  let S be IncProjStr;
  let F be Subset of the Points of S, L be LINE of S;
  pred F on L means
:: INCSP_1:def 4

  for A being POINT of S st A in F holds A on L;
end;

definition
  let S;
  let F be Subset of the Points of S, P be PLANE of S;
  pred F on P means
:: INCSP_1:def 5

  for A st A in F holds A on P;
end;

definition
  let S be IncProjStr;
  let F be Subset of the Points of S;
  attr F is linear means
:: INCSP_1:def 6

  ex L being LINE of S st F on L;
end;

definition
  let S be IncStruct;
  let F be Subset of the Points of S;
  attr F is planar means
:: INCSP_1:def 7

  ex P be PLANE of S st F on P;
end;

theorem :: INCSP_1:1
  for S being IncProjStr, L being LINE of S, A, B being POINT of S
  holds {A,B} on L iff A on L & B on L;

theorem :: INCSP_1:2
  for S being IncProjStr, L being LINE of S, A, B, C being POINT
  of S holds {A,B,C} on L iff A on L & B on L & C on L;

theorem :: INCSP_1:3
  {A,B} on P iff A on P & B on P;

theorem :: INCSP_1:4
  {A,B,C} on P iff A on P & B on P & C on P;

theorem :: INCSP_1:5
  {A,B,C,D} on P iff A on P & B on P & C on P & D on P;

theorem :: INCSP_1:6
  G c= F & F on L implies G on L;

theorem :: INCSP_1:7
  G c= F & F on P implies G on P;

theorem :: INCSP_1:8
  F on L & A on L iff F \/ {A} on L;

theorem :: INCSP_1:9
  F on P & A on P iff F \/ {A} on P;

theorem :: INCSP_1:10
  F \/ G on L iff F on L & G on L;

theorem :: INCSP_1:11
  F \/ G on P iff F on P & G on P;

theorem :: INCSP_1:12
  G c= F & F is linear implies G is linear;

theorem :: INCSP_1:13
  G c= F & F is planar implies G is planar;

:: Introduction of mode IncSpace

definition
  let S be IncProjStr;
  attr S is with_non-trivial_lines means
:: INCSP_1:def 8

  for L being LINE of S ex A,B being POINT of S st A <> B & {A,B} on L;
  attr S is linear means
:: INCSP_1:def 9

  for A,B being POINT of S ex L being LINE of S st {A,B} on L;
  attr S is up-2-rank means
:: INCSP_1:def 10

  for A,B being POINT of S, K,L being LINE
  of S st A <> B & {A,B} on K & {A,B} on L holds K = L;
end;

definition
  let S be IncStruct;
  attr S is with_non-empty_planes means
:: INCSP_1:def 11

  for P being PLANE of S ex A being POINT of S st A on P;
  attr S is planar means
:: INCSP_1:def 12

  for A,B,C being POINT of S ex P being PLANE of S st {A,B,C} on P;
  attr S is with_<=1_plane_per_3_pts means
:: INCSP_1:def 13

  for A,B,C being POINT of S,
  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;
  attr S is with_lines_inside_planes means
:: INCSP_1:def 14

  for L being LINE of S, 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;
  attr S is with_planes_intersecting_in_2_pts means
:: INCSP_1:def 15

  for A being POINT
of S, P,Q being PLANE of S st A on P & A on Q ex B being POINT of S st A <> B &
  B on P & B on Q;
  attr S is up-3-dimensional means
:: INCSP_1:def 16

  ex A,B,C,D being POINT of S st not {A,B,C,D} is planar;
  attr S is inc-compatible means
:: INCSP_1:def 17

  for A being POINT of S, L being LINE
  of S, P being PLANE of S st A on L & L on P holds A on P;
end;

definition
  let IT be IncStruct;
  attr IT is IncSpace-like means
:: INCSP_1:def 18

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

reserve a,b,c for Element of {0,1,2,3};

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

registration
  cluster strict IncSpace-like for IncStruct;
end;

definition
  mode IncSpace is IncSpace-like IncStruct;
end;

reserve S for IncSpace;
reserve A,B,C,D,E for POINT of S;
reserve K,L,L1,L2 for LINE of S;
reserve P,P1,P2,Q for PLANE of S;
reserve F for Subset of the Points of S;

::                Axioms of Incidence

theorem :: INCSP_1:14
  F on L & L on P implies F on P;

:: Collinearity of points & coplanarity of points & lines

theorem :: INCSP_1:15
  {A,A,B} is linear;

theorem :: INCSP_1:16
  {A,A,B,C} is planar;

theorem :: INCSP_1:17
  {A,B,C} is linear implies {A,B,C,D} is planar;

theorem :: INCSP_1:18
  A <> B & {A,B} on L & not C on L implies not {A,B,C} is linear;

theorem :: INCSP_1:19
  not {A,B,C} is linear & {A,B,C} on P & not D on P implies not {A
  ,B,C,D} is planar;

theorem :: INCSP_1:20
  not(ex P st K on P & L on P) implies K <> L;

theorem :: INCSP_1:21
  not(ex P st L on P & L1 on P & L2 on P) & (ex A st A on L & A on L1 &
  A on L2) implies L <> L1;

theorem :: INCSP_1:22
  L1 on P & L2 on P & not L on P & L1 <> L2 implies not(ex Q st L on Q &
  L1 on Q & L2 on Q);

::     Lines & planes

theorem :: INCSP_1:23
  (ex A st A on K & A on L) implies ex P st K on P & L on P;

theorem :: INCSP_1:24
  A <> B implies ex L st for K holds {A,B} on K iff K = L;

theorem :: INCSP_1:25
  not {A,B,C} is linear implies ex P st for Q holds {A,B,C} on Q iff P = Q;

theorem :: INCSP_1:26
  not A on L implies ex P st for Q holds A on Q & L on Q iff P = Q;

theorem :: INCSP_1:27
  K <>L & (ex A st A on K & A on L) implies ex P st for Q holds K
  on Q & L on Q iff P = Q;

::    Definitions of functions: Line, Plane

definition
  let S;
  let A,B;
  assume
 A <> B;
  func Line(A,B) -> LINE of S means
:: INCSP_1:def 19

  {A,B} on it;
end;

definition
  let S;
  let A,B,C;
  assume
 not {A,B,C} is linear;
  func Plane(A,B,C) -> PLANE of S means
:: INCSP_1:def 20

  {A,B,C} on it;
end;

definition
  let S;
  let A,L;
  assume
 not A on L;
  func Plane(A,L) -> PLANE of S means
:: INCSP_1:def 21

  A on it & L on it;
end;

definition
  let S;
  let K,L;
  assume that
 K <> L and
 ex A st A on K & A on L;
  func Plane(K,L) -> PLANE of S means
:: INCSP_1:def 22

  K on it & L on it;
end;

:: Definitional theorems of functions: Line, Plane

theorem :: INCSP_1:28
  A <> B implies Line(A,B) = Line(B,A);

theorem :: INCSP_1:29
  not {A,B,C} is linear implies Plane(A,B,C) = Plane(A,C,B);

theorem :: INCSP_1:30
  not {A,B,C} is linear implies Plane(A,B,C) = Plane(B,A,C);

theorem :: INCSP_1:31
  not {A,B,C} is linear implies Plane(A,B,C) = Plane(B,C,A);

theorem :: INCSP_1:32
  not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,A,B);

theorem :: INCSP_1:33
  not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,B,A);

theorem :: INCSP_1:34
  K <> L & (ex A st A on K & A on L) implies Plane(K,L) = Plane(L,K);

theorem :: INCSP_1:35
  A <> B & C on Line(A,B) implies {A,B,C} is linear;

theorem :: INCSP_1:36
  A <> B & A <> C & {A,B,C} is linear implies Line(A,B) = Line(A,C);

theorem :: INCSP_1:37
  not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,Line(A,B));

theorem :: INCSP_1:38
  not {A,B,C} is linear & D on Plane(A,B,C) implies {A,B,C,D} is planar;

theorem :: INCSP_1:39
  not C on L & {A,B} on L & A <> B implies Plane(C,L) = Plane(A,B,C);

theorem :: INCSP_1:40
  not {A,B,C} is linear implies Plane(A,B,C) = Plane(Line(A,B),Line(A,C) );

::   The fourth axiom of incidence

theorem :: INCSP_1:41
  ex A,B,C st {A,B,C} on P & not {A,B,C} is linear;

::    Fundamental existence theorems

theorem :: INCSP_1:42
  ex A,B,C,D st A on P & not {A,B,C,D} is planar;

theorem :: INCSP_1:43
  ex B st A <> B & B on L;

theorem :: INCSP_1:44
  A <> B implies ex C st C on P & not {A,B,C} is linear;

theorem :: INCSP_1:45
  not {A,B,C} is linear implies ex D st not {A,B,C,D} is planar;

theorem :: INCSP_1:46
  ex B,C st {B,C} on P & not {A,B,C} is linear;

theorem :: INCSP_1:47
  A <> B implies ex C,D st not {A,B,C,D} is planar;

theorem :: INCSP_1:48
  ex B,C,D st not {A,B,C,D} is planar;

theorem :: INCSP_1:49
  ex L st not A on L & L on P;

theorem :: INCSP_1:50
  A on P implies ex L,L1,L2 st L1 <> L2 & L1 on P & L2 on P & not
  L on P & A on L & A on L1 & A on L2;

theorem :: INCSP_1:51
  ex L,L1,L2 st A on L & A on L1 & A on L2 & not(ex P st L on P & L1 on
  P & L2 on P);

theorem :: INCSP_1:52
  ex P st A on P & not L on P;

theorem :: INCSP_1:53
  ex A st A on P & not A on L;

theorem :: INCSP_1:54
  ex K st not(ex P st L on P & K on P);

theorem :: INCSP_1:55
  ex P,Q st P <> Q & L on P & L on Q;

::  Intersection of lines and planes

theorem :: INCSP_1:56
  not L on P & {A,B} on L & {A,B} on P implies A = B;

theorem :: INCSP_1:57
  P <> Q implies not(ex A st A on P & A on Q) or ex L st for B holds B
  on P & B on Q iff B on L;