The abstract of the Mizar article:

Shear Theorems and Their Role in Affine Geometry

by

Jolanta Swierzynska, and

Bogdan Swierzynski

Received April 19, 1991

MML identifier: CONMETR1

[ Mizar article, MML identifier index ]

environ

 vocabulary DIRAF, ANALOAF, AFF_1, AFF_2, ANALMETR, CONMETR, CONAFFM, CONMETR1;
 notation SUBSET_1, STRUCT_0, ANALOAF, DIRAF, AFF_1, ANALMETR, AFF_2, CONAFFM,
      CONMETR;
 constructors AFF_1, AFF_2, CONAFFM, CONMETR, XBOOLE_0;
 clusters ANALMETR, ZFMISC_1, XBOOLE_0;
 requirements SUBSET;


begin
reserve X for AffinPlane;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,d,d1,d2,
        d3,d4,d5,e1,e2,x,y,z for Element of X;
reserve Y,Z,M,N,A,K,C for Subset of X;

definition let X; attr X is satisfying_minor_Scherungssatz means
:: CONMETR1:def 1
 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M // N &
         a1 in M & a3 in M & b1 in M & b3 in M & a2 in N &
         a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M &
         not b2 in M & not b4 in M & not a1 in N & not a3 in N &
         not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_minor_SCH;
end;

definition let X; attr X is satisfying_major_Scherungssatz means
:: CONMETR1:def 2
 for o,a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line &
         N is_line & o in M & o in N & a1 in M & a3 in M & b1 in M &
         b3 in M & a2 in N &
         a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M &
         not b2 in M & not b4 in M & not a1 in N & not a3 in N &
         not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_major_SCH;
end;

definition let X; attr X is satisfying_Scherungssatz means
:: CONMETR1:def 3
 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line &
         N is_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N &
         a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M &
         not b2 in M & not b4 in M & not a1 in N & not a3 in N &
         not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_SCH;
end;

definition let X; attr X is satisfying_indirect_Scherungssatz means
:: CONMETR1:def 4
 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line &
         N is_line & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N &
         a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M &
         not b1 in M & not b3 in M & not a1 in N & not a3 in N &
         not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_SCH*;
end;

definition let X; attr X is satisfying_minor_indirect_Scherungssatz means
:: CONMETR1:def 5
 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M // N
          & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N &
         a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M &
         not b1 in M & not b3 in M & not a1 in N & not a3 in N &
         not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_minor_SCH*;
end;

definition let X; attr X is satisfying_major_indirect_Scherungssatz means
:: CONMETR1:def 6
 for o,a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line & N is_line &
         o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N &
         a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M
         & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N
         & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
         a3,a4 // b3,b4;
  synonym X satisfies_major_SCH*;
end;

theorem :: CONMETR1:1
    X satisfies_SCH* iff (X satisfies_minor_SCH* & X satisfies_major_SCH*);

theorem :: CONMETR1:2
   X satisfies_SCH iff (X satisfies_minor_SCH & X satisfies_major_SCH);

theorem :: CONMETR1:3
      X satisfies_minor_SCH* implies X satisfies_minor_SCH;

 theorem :: CONMETR1:4
       X satisfies_major_SCH* implies X satisfies_major_SCH;

theorem :: CONMETR1:5
         X satisfies_SCH* implies X satisfies_SCH;

theorem :: CONMETR1:6
        X satisfies_des implies X satisfies_minor_SCH;

theorem :: CONMETR1:7
         X satisfies_DES implies X satisfies_major_SCH;

theorem :: CONMETR1:8
X satisfies_DES iff X satisfies_SCH;

theorem :: CONMETR1:9
        X satisfies_pap iff X satisfies_minor_SCH*;

theorem :: CONMETR1:10
          X satisfies_PAP iff X satisfies_major_SCH*;

theorem :: CONMETR1:11
          X satisfies_PPAP iff X satisfies_SCH*;

theorem :: CONMETR1:12
         X satisfies_major_SCH* implies X satisfies_minor_SCH*;

reserve X for OrtAfPl;
reserve o',a',a1',a2',a3',a4',b',b1',b2',b3',b4',c',c1'
 for Element of X;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1
        for Element of Af(X);
reserve M',N' for Subset of X;
reserve A,M,N for Subset of Af(X);

theorem :: CONMETR1:13
             Af(X) satisfies_SCH iff SCH_holds_in X;

theorem :: CONMETR1:14
             TDES_holds_in X iff Af(X) satisfies_TDES;

theorem :: CONMETR1:15
             Af(X) satisfies_des iff des_holds_in X;

theorem :: CONMETR1:16
            PAP_holds_in X iff Af(X) satisfies_PAP;

theorem :: CONMETR1:17
             DES_holds_in X iff Af(X) satisfies_DES;