The abstract of the Mizar article:

Axioms of Incidency

by

Wojciech A. Trybulec

Received April 14, 1989

MML identifier: INCSP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, BOOLE, INCSP_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1;
 constructors DOMAIN_1, RELSET_1, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


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, is_collinear, is_coplanar

 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;
  synonym F is_collinear;
 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;
  synonym F is_coplanar;
 end;

::  Definitional theorems of predicates: on, is_collinear, is_coplanar

canceled 10;

theorem :: INCSP_1:11
 {A,B} on L iff A on L & B on L;

theorem :: INCSP_1:12
 {A,B,C} on L iff A on L & B on L & C on L;

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

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

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

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

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

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

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

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

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

theorem :: INCSP_1:22
   G c= F & F is_collinear implies G is_collinear;

theorem :: INCSP_1:23
   G c= F & F is_coplanar implies G is_coplanar;
 reserve a,b,c for Element of Po;
 reserve k,l for Element of Li;
 reserve p,q for Element of Pl;

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

    (for L being LINE of IT ex A,B being POINT of IT st A <> B & {A,B} on L) &
    (for A,B being POINT of IT ex L being LINE of IT st {A,B} on L) &
    (for A,B being (POINT of IT), K,L being LINE of IT
      st A <> B & {A,B} on K & {A,B} on L holds K = L) &
    (for P being PLANE of IT ex A being POINT of IT st A on P) &
    (for A,B,C being POINT of IT ex P being PLANE of IT st {A,B,C} on P) &
    (for A,B,C being (POINT of IT), P,Q being PLANE of IT
      st not {A,B,C} is_collinear & {A,B,C} on P & {A,B,C} on Q
       holds P = Q) &
    (for L being (LINE of IT), P being PLANE of IT
      st ex A,B being POINT of IT st A <> B & {A,B} on L & {A,B} on P
       holds L on P) &
    (for A being (POINT of IT), P,Q being PLANE of IT
      st A on P & A on Q ex B being POINT of IT st A <> B & B on P & B on Q) &
    (ex A,B,C,D being POINT of IT st not {A,B,C,D} is_coplanar) &
    (for A being (POINT of IT), L being (LINE of IT), P being PLANE of IT
      st A on L & L on P holds A on P);
 end;

definition
 cluster strict IncSpace-like 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 Incidency

canceled 11;

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

::     Collinearity of points & coplanariy of points & lines

theorem :: INCSP_1:36
 {A,A,B} is_collinear;

theorem :: INCSP_1:37
 {A,A,B,C} is_coplanar;

theorem :: INCSP_1:38
 {A,B,C} is_collinear implies {A,B,C,D} is_coplanar;

theorem :: INCSP_1:39
 A <> B & {A,B} on L & not C on L implies not {A,B,C} is_collinear;

theorem :: INCSP_1:40
 not {A,B,C} is_collinear & {A,B,C} on P & not D on P implies
  not {A,B,C,D} is_coplanar;

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

theorem :: INCSP_1:42
   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:43
   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:44
 ex P st A on P & L on P;

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

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

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

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

theorem :: INCSP_1:49
 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 9
   {A,B} on it;
end;

definition let S; let A,B,C;
 assume  not {A,B,C} is_collinear;
 func Plane(A,B,C) -> PLANE of S means
:: INCSP_1:def 10
   {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 11
   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 12
   K on it & L on it;
end;

::    Definitional theorems of functions: Line, Plane

canceled 7;

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

theorem :: INCSP_1:58
 not {A,B,C} is_collinear implies Plane(A,B,C) = Plane(A,C,B);

theorem :: INCSP_1:59
 not {A,B,C} is_collinear implies Plane(A,B,C) = Plane(B,A,C);

theorem :: INCSP_1:60
   not {A,B,C} is_collinear implies Plane(A,B,C) = Plane(B,C,A);

theorem :: INCSP_1:61
 not {A,B,C} is_collinear implies Plane(A,B,C) = Plane(C,A,B);

theorem :: INCSP_1:62
   not {A,B,C} is_collinear implies Plane(A,B,C) = Plane(C,B,A);

canceled;

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

theorem :: INCSP_1:65
 A <> B & C on Line(A,B) implies {A,B,C} is_collinear;

theorem :: INCSP_1:66
   A <> B & A <> C & {A,B,C} is_collinear implies Line(A,B) = Line(A,C);

theorem :: INCSP_1:67
   not {A,B,C} is_collinear implies Plane(A,B,C) = Plane(C,Line(A,B));

theorem :: INCSP_1:68
   not {A,B,C} is_collinear & D on Plane(A,B,C) implies {A,B,C,D} is_coplanar;

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

theorem :: INCSP_1:70
   not {A,B,C} is_collinear implies Plane(A,B,C) = Plane(Line(A,B),Line(A,C));

::   The fourth axiom of incidency

theorem :: INCSP_1:71
 ex A,B,C st {A,B,C} on P & not {A,B,C} is_collinear;

::    Fundamental existence theorems

theorem :: INCSP_1:72
   ex A,B,C,D st A on P & not {A,B,C,D} is_coplanar;

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

theorem :: INCSP_1:74
 A <> B implies ex C st C on P & not {A,B,C} is_collinear;

theorem :: INCSP_1:75
 not {A,B,C} is_collinear implies ex D st not {A,B,C,D} is_coplanar;

theorem :: INCSP_1:76
 ex B,C st {B,C} on P & not {A,B,C} is_collinear;

theorem :: INCSP_1:77
 A <> B implies (ex C,D st not {A,B,C,D} is_coplanar);

theorem :: INCSP_1:78
   ex B,C,D st not {A,B,C,D} is_coplanar;

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

theorem :: INCSP_1:80
 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:81
   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:82
   ex P st A on P & not L on P;

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

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

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

::  Intersection of lines and planes

canceled;

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

theorem :: INCSP_1:88
   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);