semi_af1.miz

    begin

    definition

      let IT be non empty AffinStruct;

      :: SEMI_AF1:def1

      attr IT is Semi_Affine_Space-like means

      : Def1: (for a,b be Element of IT holds (a,b) // (b,a)) & (for a,b,c be Element of IT holds (a,b) // (c,c)) & (for a,b,p,q,r,s be Element of IT holds (a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s))) & (for a,b,c be Element of IT holds ((a,b) // (a,c) implies (b,a) // (b,c))) & (ex a,b,c be Element of IT st not (a,b) // (a,c)) & (for a,b,p be Element of IT holds ex q be Element of IT st ((a,b) // (p,q) & (a,p) // (b,q))) & (for o,a be Element of IT holds (ex p be Element of IT st (for b,c be Element of IT holds (o,a) // (o,p) & (ex d be Element of IT st ((o,p) // (o,b) implies (o,c) // (o,d) & (p,c) // (b,d)))))) & (for o,a,a9,b,b9,c,c9 be Element of IT holds ( not (o,a) // (o,b) & not (o,a) // (o,c) & (o,a) // (o,a9) & (o,b) // (o,b9) & (o,c) // (o,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) implies (b,c) // (b9,c9))) & (for a,a9,b,b9,c,c9 be Element of IT holds ( not (a,a9) // (a,b) & not (a,a9) // (a,c) & (a,a9) // (b,b9) & (a,a9) // (c,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) implies (b,c) // (b9,c9))) & (for a1,a2,a3,b1,b2,b3 be Element of IT holds ((a1,a2) // (a1,a3) & (b1,b2) // (b1,b3) & (a1,b2) // (a2,b1) & (a2,b3) // (a3,b2) implies (a3,b1) // (a1,b3))) & for a,b,c,d be Element of IT holds ( not (a,b) // (a,c) & (a,b) // (c,d) & (a,c) // (b,d) implies not (a,d) // (b,c));

    end

    registration

      cluster Semi_Affine_Space-like for non empty AffinStruct;

      existence

      proof

        consider SAS be AffinPlane such that

         A1: ((for o,a,a9,b,b9,c,c9 be Element of SAS holds ( not (o,a) // (o,b) & not (o,a) // (o,c) & (o,a) // (o,a9) & (o,b) // (o,b9) & (o,c) // (o,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) implies (b,c) // (b9,c9))) & for a,a9,b,b9,c,c9 be Element of SAS holds ( not (a,a9) // (a,b) & not (a,a9) // (a,c) & (a,a9) // (b,b9) & (a,a9) // (c,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) implies (b,c) // (b9,c9))) & ((for a1,a2,a3,b1,b2,b3 be Element of SAS holds ((a1,a2) // (a1,a3) & (b1,b2) // (b1,b3) & (a1,b2) // (a2,b1) & (a2,b3) // (a3,b2) implies (a3,b1) // (a1,b3))) & for a,b,c,d be Element of SAS holds ( not (a,b) // (a,c) & (a,b) // (c,d) & (a,c) // (b,d) implies not (a,d) // (b,c))) by PARDEPAP: 4;

        reconsider AS = SAS as non empty AffinStruct;

        take AS;

        thus for a,b be Element of AS holds (a,b) // (b,a) by DIRAF: 40;

        thus thesis by A1, DIRAF: 40, PARDEPAP: 5;

      end;

    end

    definition

      mode Semi_Affine_Space is Semi_Affine_Space-like non empty AffinStruct;

    end

    reserve SAS for Semi_Affine_Space;

    reserve a,a9,a1,a2,a3,a4,b,b9,c,c9,d,d9,d1,d2,o,p,p1,p2,q,r,r1,r2,s,x,y,t,z for Element of SAS;

    theorem :: SEMI_AF1:1



     Th1: (a,b) // (a,b)

    proof

      (b,a) // (b,b) by Def1;

      hence thesis by Def1;

    end;

    theorem :: SEMI_AF1:2



     Th2: (a,b) // (c,d) implies (c,d) // (a,b)

    proof

      assume

       A1: (a,b) // (c,d);

      (a,b) // (a,b) by Th1;

      then a <> b implies (c,d) // (a,b) by A1, Def1;

      hence thesis by Def1;

    end;

    theorem :: SEMI_AF1:3



     Th3: (a,a) // (b,c)

    proof

      (b,c) // (a,a) by Def1;

      hence thesis by Th2;

    end;

    theorem :: SEMI_AF1:4



     Th4: (a,b) // (c,d) implies (b,a) // (c,d)

    proof

      assume

       A1: (a,b) // (c,d);

      (a,b) // (b,a) by Def1;

      then a <> b implies (b,a) // (c,d) by A1, Def1;

      hence thesis by A1;

    end;

    theorem :: SEMI_AF1:5



     Th5: (a,b) // (c,d) implies (a,b) // (d,c)

    proof

      assume (a,b) // (c,d);

      then (c,d) // (a,b) by Th2;

      then (d,c) // (a,b) by Th4;

      hence thesis by Th2;

    end;

    theorem :: SEMI_AF1:6



     Th6: (a,b) // (c,d) implies (b,a) // (c,d) & (a,b) // (d,c) & (b,a) // (d,c) & (c,d) // (a,b) & (d,c) // (a,b) & (c,d) // (b,a) & (d,c) // (b,a)

    proof

      assume (a,b) // (c,d);

      then (c,d) // (a,b) by Th2;

      then

       A1: (d,c) // (a,b) by Th4;

      then

       A2: (d,c) // (b,a) by Th5;

      then (c,d) // (b,a) by Th4;

      hence thesis by A1, A2, Th2, Th4;

    end;

    theorem :: SEMI_AF1:7



     Th7: (a,b) // (a,c) implies (a,c) // (a,b) & (b,a) // (a,c) & (a,b) // (c,a) & (a,c) // (b,a) & (b,a) // (c,a) & (c,a) // (a,b) & (c,a) // (b,a) & (b,a) // (b,c) & (a,b) // (b,c) & (b,a) // (c,b) & (b,c) // (b,a) & (a,b) // (c,b) & (c,b) // (b,a) & (b,c) // (a,b) & (c,b) // (a,b) & (c,a) // (c,b) & (a,c) // (c,b) & (c,a) // (b,c) & (a,c) // (b,c) & (c,b) // (c,a) & (b,c) // (c,a) & (c,b) // (a,c) & (b,c) // (a,c)

    proof

      assume

       A1: (a,b) // (a,c);

      then (a,c) // (a,b) by Th2;

      then

       A2: (c,a) // (c,b) by Def1;

      (b,a) // (b,c) by A1, Def1;

      hence thesis by A1, A2, Th6;

    end;

    theorem :: SEMI_AF1:8



     Th8: a <> b & (p,q) // (a,b) & (a,b) // (r,s) implies (p,q) // (r,s)

    proof

      assume that

       A1: a <> b and

       A2: (p,q) // (a,b) and

       A3: (a,b) // (r,s);

      (a,b) // (p,q) by A2, Th6;

      hence thesis by A1, A3, Def1;

    end;

    theorem :: SEMI_AF1:9

     not (a,b) // (a,d) implies a <> b & b <> d & d <> a by Def1, Th1, Th3;

    theorem :: SEMI_AF1:10

     not (a,b) // (p,q) implies a <> b & p <> q by Def1, Th3;

    theorem :: SEMI_AF1:11

    (a,b) // (a,x) & (b,c) // (b,x) & (c,a) // (c,x) implies (a,b) // (a,c)

    proof

      assume that

       A1: (a,b) // (a,x) and

       A2: (b,c) // (b,x) and

       A3: (c,a) // (c,x);

      now

        assume

         A4: a <> x;

        (a,x) // (a,b) & (a,x) // (a,c) by A1, A3, Th7;

        hence thesis by A4, Def1;

      end;

      hence thesis by A2, Th7;

    end;

    theorem :: SEMI_AF1:12



     Th12: not (a,b) // (a,c) & p <> q implies not (p,q) // (p,a) or not (p,q) // (p,b) or not (p,q) // (p,c)

    proof

      assume that

       A1: not (a,b) // (a,c) and

       A2: p <> q;

      now

        assume that

         A3: a <> p and

         A4: (p,q) // (p,a) and

         A5: (p,q) // (p,b) and

         A6: (p,q) // (p,c);

        (p,a) // (p,c) by A2, A4, A6, Def1;

        then

         A7: (a,p) // (a,c) by Def1;

        (p,a) // (p,b) by A2, A4, A5, Def1;

        then (a,p) // (a,b) by Def1;

        hence contradiction by A1, A3, A7, Def1;

      end;

      hence thesis by A1, A2, Def1;

    end;

    theorem :: SEMI_AF1:13



     Th13: p <> q implies ex r st not (p,q) // (p,r)

    proof

      consider a, b, c such that

       A1: not (a,b) // (a,c) by Def1;

      assume p <> q;

      then not (p,q) // (p,a) or not (p,q) // (p,b) or not (p,q) // (p,c) by A1, Th12;

      hence thesis;

    end;

    theorem :: SEMI_AF1:14



     Th14: not (a,b) // (a,c) implies not (a,b) // (c,a) & not (b,a) // (a,c) & not (b,a) // (c,a) & not (a,c) // (a,b) & not (a,c) // (b,a) & not (c,a) // (a,b) & not (c,a) // (b,a) & not (b,a) // (b,c) & not (b,a) // (c,b) & not (a,b) // (b,c) & not (a,b) // (c,b) & not (b,c) // (b,a) & not (b,c) // (a,b) & not (c,b) // (a,b) & not (c,b) // (b,a) & not (c,b) // (c,a) & not (c,b) // (a,c) & not (b,c) // (c,a) & not (b,c) // (a,c) & not (c,a) // (c,b) & not (c,a) // (b,c) & not (a,c) // (b,c) & not (a,c) // (c,b)

    proof

      assume

       A1: not (a,b) // (a,c);

       A2:

      now

        assume (a,c) // (c,b);

        then (c,a) // (c,b) by Th6;

        hence contradiction by A1, Th7;

      end;

      assume

       A3: not thesis;

       not (b,a) // (b,c) by A1, Th7;

      hence thesis by A1, A3, A2, Th6;

    end;

    theorem :: SEMI_AF1:15



     Th15: not (a,b) // (c,d) & (a,b) // (p,q) & (c,d) // (r,s) & p <> q & r <> s implies not (p,q) // (r,s)

    proof

      assume that

       A1: not (a,b) // (c,d) and

       A2: (a,b) // (p,q) and

       A3: (c,d) // (r,s) and

       A4: p <> q and

       A5: r <> s;

      assume (p,q) // (r,s);

      then (a,b) // (r,s) by A2, A4, Th8;

      then

       A6: (r,s) // (a,b) by Th6;

      (r,s) // (c,d) by A3, Th6;

      hence contradiction by A1, A5, A6, Def1;

    end;

    theorem :: SEMI_AF1:16



     Th16: not (a,b) // (a,c) & (a,b) // (p,q) & (a,c) // (p,r) & (b,c) // (q,r) & p <> q implies not (p,q) // (p,r)

    proof

      assume that

       A1: not (a,b) // (a,c) and

       A2: (a,b) // (p,q) and

       A3: (a,c) // (p,r) and

       A4: (b,c) // (q,r) and

       A5: p <> q;

      now

        assume p = r;

        then

         A6: (p,q) // (b,c) by A4, Th6;

        (p,q) // (a,b) by A2, Th6;

        then (a,b) // (b,c) by A5, A6, Def1;

        then (b,a) // (b,c) by Th4;

        hence contradiction by A1, Th7;

      end;

      hence thesis by A1, A2, A3, A5, Th15;

    end;

    theorem :: SEMI_AF1:17



     Th17: not (a,b) // (a,c) & (a,c) // (p,r) & (b,c) // (p,r) implies p = r

    proof

      assume that

       A1: ( not (a,b) // (a,c)) & (a,c) // (p,r) and

       A2: (b,c) // (p,r);



       A3: (p,r) // (b,c) by A2, Th6;

      ( not (a,c) // (b,c)) & (p,r) // (a,c) by A1, Th6, Th14;

      hence thesis by A3, Def1;

    end;

    theorem :: SEMI_AF1:18



     Th18: not (p,q) // (p,r1) & (p,r1) // (p,r2) & (q,r1) // (q,r2) implies r1 = r2

    proof

      assume that

       A1: ( not (p,q) // (p,r1)) & (p,r1) // (p,r2) and

       A2: (q,r1) // (q,r2);



       A3: (r1,r2) // (r1,q) by A2, Th14;

      ( not (r1,p) // (r1,q)) & (r1,r2) // (r1,p) by A1, Th14;

      hence thesis by A3, Def1;

    end;

    theorem :: SEMI_AF1:19



     Th19: not (a,b) // (a,c) & (a,b) // (p,q) & (a,c) // (p,r1) & (a,c) // (p,r2) & (b,c) // (q,r1) & (b,c) // (q,r2) implies r1 = r2

    proof

      assume that

       A1: not (a,b) // (a,c) and

       A2: (a,b) // (p,q) and

       A3: (a,c) // (p,r1) and

       A4: (a,c) // (p,r2) and

       A5: (b,c) // (q,r1) and

       A6: (b,c) // (q,r2);

       A7:

      now

        b <> c by A1, Th1;

        then

         A8: (q,r1) // (q,r2) by A5, A6, Def1;

        a <> c by A1, Def1;

        then

         A9: (p,r1) // (p,r2) by A3, A4, Def1;

        assume p <> q;

        then not (p,q) // (p,r1) by A1, A2, A3, A5, Th16;

        hence thesis by A9, A8, Th18;

      end;

      now

        assume

         A10: p = q;

        then p = r1 by A1, A3, A5, Th17;

        hence thesis by A1, A4, A6, A10, Th17;

      end;

      hence thesis by A7;

    end;

    theorem :: SEMI_AF1:20

    a = b or c = d or a = c & b = d or a = d & b = c implies (a,b) // (c,d) by Def1, Th1, Th3;

    theorem :: SEMI_AF1:21

    a = b or a = c or b = c implies (a,b) // (a,c) by Def1, Th1, Th3;

    definition

      let SAS, a, b, c;

      :: SEMI_AF1:def2

      pred a,b,c are_collinear means (a,b) // (a,c);

    end

    theorem :: SEMI_AF1:22



     Th22: (a1,a2,a3) are_collinear implies (a1,a3,a2) are_collinear & (a2,a1,a3) are_collinear & (a2,a3,a1) are_collinear & (a3,a1,a2) are_collinear & (a3,a2,a1) are_collinear by Th7;

    theorem :: SEMI_AF1:23



     Th23: not (a,b,c) are_collinear & (a,b) // (p,q) & (a,c) // (p,r) & p <> q & p <> r implies not (p,q,r) are_collinear by Th15;

    theorem :: SEMI_AF1:24



     Th24: a = b or b = c or c = a implies (a,b,c) are_collinear by Def1, Th1, Th3;

    theorem :: SEMI_AF1:25



     Th25: p <> q implies ex r st not (p,q,r) are_collinear

    proof

      assume p <> q;

      then

      consider r such that

       A1: not (p,q) // (p,r) by Th13;

      take r;

      thus thesis by A1;

    end;

    theorem :: SEMI_AF1:26



     Th26: (a,b,c) are_collinear & (a,b,d) are_collinear implies (a,b) // (c,d)

    proof

      assume that

       A1: (a,b,c) are_collinear and

       A2: (a,b,d) are_collinear ;

      now

        assume that

         A3: a <> b and

         A4: a <> c;



         A5: (a,b) // (a,c) by A1;

        (a,b) // (a,d) by A2;

        then (a,c) // (a,d) by A3, A5, Def1;

        then (a,c) // (c,d) by Th7;

        hence thesis by A4, A5, Th8;

      end;

      hence thesis by A2, Th3;

    end;

    theorem :: SEMI_AF1:27



     Th27: not (a,b,c) are_collinear & (a,b) // (c,d) implies not (a,b,d) are_collinear

    proof

      assume that

       A1: not (a,b,c) are_collinear and

       A2: (a,b) // (c,d);

      now

        assume that

         A3: c <> d and

         A4: (a,b,d) are_collinear ;

        (a,b) // (a,d) by A4;

        then

         A5: (a,b) // (d,a) by Th6;



         A6: (a,b) // (d,c) by A2, Th6;



         A7: (a,c) // (c,a) by Def1;



         A8: not (a,b) // (a,c) by A1;

        then a <> b by Th3;

        then

         A9: (d,c) // (d,a) by A6, A5, Def1;

        c <> a by A8, Def1;

        then not (c,d) // (c,a) by A2, A3, A8, A7, Th15;

        hence contradiction by A9, Th7;

      end;

      hence thesis by A1;

    end;

    theorem :: SEMI_AF1:28



     Th28: not (a,b,c) are_collinear & (a,b) // (c,d) & c <> d & (c,d,x) are_collinear implies not (a,b,x) are_collinear by Th8, Th27;

    theorem :: SEMI_AF1:29

     not (o,a,b) are_collinear & (o,a,x) are_collinear & (o,b,x) are_collinear implies o = x

    proof

      assume that

       A1: not (o,a,b) are_collinear and

       A2: (o,a,x) are_collinear and

       A3: (o,b,x) are_collinear ;

      (b,o,x) are_collinear by A3, Th22;

      then

       A4: (b,o) // (b,x);

      (o,a) // (o,x) by A2;

      then

       A5: (a,o) // (a,x) by Th14;

       not (a,b,o) are_collinear by A1, Th22;

      then not (a,b) // (a,o);

      hence thesis by A5, A4, Th18;

    end;

    theorem :: SEMI_AF1:30

    o <> a & o <> b & (o,a,b) are_collinear & (o,a,a9) are_collinear & (o,b,b9) are_collinear implies (a,b) // (a9,b9)

    proof

      assume that

       A1: o <> a and

       A2: o <> b and

       A3: (o,a,b) are_collinear and

       A4: (o,a,a9) are_collinear and

       A5: (o,b,b9) are_collinear ;

       A6:

      now



         A7: (o,a) // (o,b) by A3;

        (o,a) // (o,a9) by A4;

        then

         A8: (o,b) // (o,a9) by A1, A7, Def1;

        (o,b) // (o,b9) by A5;

        then (o,a9) // (o,b9) by A2, A8, Def1;

        then

         A9: (o,a9) // (a9,b9) by Th7;

        (o,b) // (a,b) by A7, Th7;

        then

         A10: (a,b) // (o,a9) by A2, A8, Def1;

        assume o <> a9;

        hence thesis by A10, A9, Th8;

      end;

      now

        assume

         A11: o = a9;

        then (a9,a) // (a9,b) by A3;

        then

         A12: (a,b) // (a9,b) by Th7;

        (a9,b) // (a9,b9) by A5, A11;

        hence thesis by A2, A11, A12, Th8;

      end;

      hence thesis by A6;

    end;

    theorem :: SEMI_AF1:31

     not (a,b) // (c,d) & (a,b,p1) are_collinear & (a,b,p2) are_collinear & (c,d,p1) are_collinear & (c,d,p2) are_collinear implies p1 = p2

    proof

      assume that

       A1: not (a,b) // (c,d) and

       A2: (a,b,p1) are_collinear & (a,b,p2) are_collinear and

       A3: (c,d,p1) are_collinear & (c,d,p2) are_collinear ;

      (c,d) // (p1,p2) by A3, Th26;

      then

       A4: (p1,p2) // (c,d) by Th6;

      (a,b) // (p1,p2) by A2, Th26;

      then (p1,p2) // (a,b) by Th6;

      hence thesis by A1, A4, Def1;

    end;

    theorem :: SEMI_AF1:32



     Th32: a <> b & (a,b,c) are_collinear & (a,b) // (c,d) implies (a,c) // (b,d)

    proof

      assume that

       A1: a <> b and

       A2: (a,b,c) are_collinear and

       A3: (a,b) // (c,d);

      now



         A4: (a,b) // (a,c) by A2;

        then (a,b) // (c,b) by Th7;

        then (c,b) // (c,d) by A1, A3, Def1;

        then

         A5: (b,c) // (b,d) by Th7;

        assume

         A6: b <> c;

        (b,c) // (a,c) by A4, Th7;

        hence thesis by A6, A5, Def1;

      end;

      hence thesis by A3;

    end;

    theorem :: SEMI_AF1:33



     Th33: a <> b & (a,b,c) are_collinear & (a,b) // (c,d) implies (c,b) // (c,d)

    proof

      assume that

       A1: a <> b and

       A2: (a,b,c) are_collinear and

       A3: (a,b) // (c,d);

      now

        (a,b) // (a,c) by A2;

        then

         A4: (a,c) // (c,b) & (a,c) // (c,d) by A1, A3, Def1, Th7;

        assume a <> c;

        hence thesis by A4, Def1;

      end;

      hence thesis by A3;

    end;

    theorem :: SEMI_AF1:34



     Th34: not (o,a,c) are_collinear & (o,a,b) are_collinear & (o,c,d1) are_collinear & (o,c,d2) are_collinear & (a,c) // (b,d1) & (a,c) // (b,d2) implies d1 = d2 by Th19;

    theorem :: SEMI_AF1:35

    a <> b & (a,b,c) are_collinear & (a,b,d) are_collinear implies (a,c,d) are_collinear by Def1;

    definition

      let SAS, a, b, c, d;

      :: SEMI_AF1:def3

      pred parallelogram a,b,c,d means not (a,b,c) are_collinear & (a,b) // (c,d) & (a,c) // (b,d);

    end

    theorem :: SEMI_AF1:36



     Th36: parallelogram (a,b,c,d) implies a <> b & a <> c & c <> b & a <> d & b <> d & c <> d

    proof

      assume

       A1: parallelogram (a,b,c,d);

      then not (a,b,c) are_collinear ;

      hence a <> b & a <> c & c <> b by Th24;

       A2:

      now

        assume a = d;

        then (a,b) // (c,a) by A1;

        then

         A3: (a,b) // (a,c) by Th6;

         not (a,b,c) are_collinear by A1;

        hence contradiction by A3;

      end;

       A4:

      now

        assume c = d;

        then (a,c) // (b,c) by A1;

        then (c,a) // (c,b) by Th6;

        then

         A5: (c,a,b) are_collinear ;

         not (a,b,c) are_collinear by A1;

        hence contradiction by A5, Th22;

      end;

       A6:

      now

        assume b = d;

        then (a,b) // (c,b) by A1;

        then (b,a) // (b,c) by Th6;

        then

         A7: (b,a,c) are_collinear ;

         not (a,b,c) are_collinear by A1;

        hence contradiction by A7, Th22;

      end;

      assume not thesis;

      hence contradiction by A2, A6, A4;

    end;

    theorem :: SEMI_AF1:37



     Th37: parallelogram (a,b,c,d) implies not (a,b,c) are_collinear & not (b,a,d) are_collinear & not (c,d,a) are_collinear & not (d,c,b) are_collinear

    proof



       A1: (a,b) // (b,a) by Def1;

      assume

       A2: parallelogram (a,b,c,d);

      hence not (a,b,c) are_collinear ;



       A3: b <> a & b <> d by A2, Th36;

      (a,c) // (b,d) by A2;

      then

       A4: (a,c) // (d,b) by Th6;

      (a,b) // (c,d) by A2;

      then

       A5: (a,b) // (d,c) by Th6;

      ( not (a,b,c) are_collinear ) & (a,c) // (b,d) by A2;

      hence not (b,a,d) are_collinear by A1, A3, Th23;



       A6: (a,c) // (c,a) by Def1;



       A7: c <> d & c <> a by A2, Th36;

      ( not (a,b,c) are_collinear ) & (a,b) // (c,d) by A2;

      hence not (c,d,a) are_collinear by A6, A7, Th23;



       A8: d <> b by A2, Th36;

      ( not (a,b,c) are_collinear ) & c <> d by A2, Th36;

      hence thesis by A5, A4, A8, Th23;

    end;

    theorem :: SEMI_AF1:38



     Th38: parallelogram (a1,a2,a3,a4) implies not (a1,a2,a3) are_collinear & not (a1,a3,a2) are_collinear & not (a1,a2,a4) are_collinear & not (a1,a4,a2) are_collinear & not (a1,a3,a4) are_collinear & not (a1,a4,a3) are_collinear & not (a2,a1,a3) are_collinear & not (a2,a3,a1) are_collinear & not (a2,a1,a4) are_collinear & not (a2,a4,a1) are_collinear & not (a2,a3,a4) are_collinear & not (a2,a4,a3) are_collinear & not (a3,a1,a2) are_collinear & not (a3,a2,a1) are_collinear & not (a3,a1,a4) are_collinear & not (a3,a4,a1) are_collinear & not (a3,a2,a4) are_collinear & not (a3,a4,a2) are_collinear & not (a4,a1,a2) are_collinear & not (a4,a2,a1) are_collinear & not (a4,a1,a3) are_collinear & not (a4,a3,a1) are_collinear & not (a4,a2,a3) are_collinear & not (a4,a3,a2) are_collinear

    proof

      assume

       A1: parallelogram (a1,a2,a3,a4);

      then

       A2: ( not (a3,a4,a1) are_collinear ) & not (a4,a3,a2) are_collinear by Th37;

      ( not (a1,a2,a3) are_collinear ) & not (a2,a1,a4) are_collinear by A1, Th37;

      hence thesis by A2, Th22;

    end;

    theorem :: SEMI_AF1:39



     Th39: parallelogram (a,b,c,d) implies not (a,b,x) are_collinear or not (c,d,x) are_collinear

    proof

      assume

       A1: parallelogram (a,b,c,d);

      then

       A2: c <> d by Th36;

      ( not (a,b,c) are_collinear ) & (a,b) // (c,d) by A1;

      hence thesis by A2, Th28;

    end;

    theorem :: SEMI_AF1:40

     parallelogram (a,b,c,d) implies parallelogram (a,c,b,d) by Th38;

    theorem :: SEMI_AF1:41

     parallelogram (a,b,c,d) implies parallelogram (c,d,a,b) by Th6, Th38;

    theorem :: SEMI_AF1:42

     parallelogram (a,b,c,d) implies parallelogram (b,a,d,c) by Th6, Th38;

    theorem :: SEMI_AF1:43



     Th43: parallelogram (a,b,c,d) implies parallelogram (a,c,b,d) & parallelogram (c,d,a,b) & parallelogram (b,a,d,c) & parallelogram (c,a,d,b) & parallelogram (d,b,c,a) & parallelogram (b,d,a,c) by Th38, Th6;

    theorem :: SEMI_AF1:44



     Th44: not (a,b,c) are_collinear implies ex d st parallelogram (a,b,c,d)

    proof

      assume

       A1: not (a,b,c) are_collinear ;

      consider d such that

       A2: (a,b) // (c,d) & (a,c) // (b,d) by Def1;

      take d;

      thus thesis by A1, A2;

    end;

    theorem :: SEMI_AF1:45



     Th45: parallelogram (a,b,c,d1) & parallelogram (a,b,c,d2) implies d1 = d2

    proof

      assume that

       A1: parallelogram (a,b,c,d1) and

       A2: parallelogram (a,b,c,d2);

       not (b,c,a) are_collinear by A1, Th38;

      then

       A3: not (b,c) // (b,a);

      (a,c) // (b,d2) by A2;

      then

       A4: (c,a) // (b,d2) by Th6;

      (a,b) // (c,d2) by A2;

      then

       A5: (b,a) // (c,d2) by Th6;

      (a,c) // (b,d1) by A1;

      then

       A6: (c,a) // (b,d1) by Th6;

      (a,b) // (c,d1) by A1;

      then

       A7: (b,a) // (c,d1) by Th6;

      (b,c) // (c,b) by Def1;

      hence thesis by A3, A7, A5, A6, A4, Th19;

    end;

    theorem :: SEMI_AF1:46



     Th46: parallelogram (a,b,c,d) implies not (a,d) // (b,c)

    proof

      assume

       A1: parallelogram (a,b,c,d);

      then not (a,b,c) are_collinear ;

      then

       A2: not (a,b) // (a,c);

      (a,b) // (c,d) & (a,c) // (b,d) by A1;

      hence thesis by A2, Def1;

    end;

    theorem :: SEMI_AF1:47



     Th47: parallelogram (a,b,c,d) implies not parallelogram (a,b,d,c)

    proof

      assume

       A1: parallelogram (a,b,c,d);

      then not (a,b,c) are_collinear ;

      then

       A2: not (a,b) // (a,c);

      assume not thesis;

      then

       A3: (a,d) // (b,c);

      (a,b) // (c,d) & (a,c) // (b,d) by A1;

      hence contradiction by A3, A2, Def1;

    end;

    theorem :: SEMI_AF1:48



     Th48: a <> b implies ex c st (a,b,c) are_collinear & c <> a & c <> b

    proof

      assume a <> b;

      then

      consider p such that

       A1: not (a,b,p) are_collinear by Th25;

      consider q such that

       A2: parallelogram (a,b,p,q) by A1, Th44;

       not (p,q,b) are_collinear by A2, Th38;

      then

      consider c such that

       A3: parallelogram (p,q,b,c) by Th44;

      take c;



       A4: (p,q) // (b,c) by A3;

      p <> q & (a,b) // (p,q) by A2, Th36;

      then (a,b) // (b,c) by A4, Th8;

      then (b,a) // (b,c) by Th6;

      then

       A5: (b,a,c) are_collinear ;



       A6: not (a,q) // (b,p) by A2, Th46;

      (p,b) // (q,c) & not (b,c,p) are_collinear by A3, Th37;

      hence thesis by A6, A5, Th6, Th22, Th24;

    end;

    theorem :: SEMI_AF1:49



     Th49: parallelogram (a,a9,b,b9) & parallelogram (a,a9,c,c9) implies (b,c) // (b9,c9)

    proof

      assume that

       A1: parallelogram (a,a9,b,b9) and

       A2: parallelogram (a,a9,c,c9);



       A3: (a,a9) // (c,c9) & (a,c) // (a9,c9) by A2;

       not (a,a9,c) are_collinear by A2;

      then

       A4: not (a,a9) // (a,c);

       not (a,a9,b) are_collinear by A1;

      then

       A5: not (a,a9) // (a,b);

      (a,a9) // (b,b9) & (a,b) // (a9,b9) by A1;

      hence thesis by A5, A4, A3, Def1;

    end;

    theorem :: SEMI_AF1:50



     Th50: not (b,b9,c) are_collinear & parallelogram (a,a9,b,b9) & parallelogram (a,a9,c,c9) implies parallelogram (b,b9,c,c9)

    proof

      assume that

       A1: not (b,b9,c) are_collinear and

       A2: parallelogram (a,a9,b,b9) and

       A3: parallelogram (a,a9,c,c9);



       A4: (a,a9) // (c,c9) by A3;

      a <> a9 & (a,a9) // (b,b9) by A2, Th36;

      then

       A5: (b,b9) // (c,c9) by A4, Def1;

      (b,c) // (b9,c9) by A2, A3, Th49;

      hence thesis by A1, A5;

    end;

    theorem :: SEMI_AF1:51



     Th51: (a,b,c) are_collinear & b <> c & parallelogram (a,a9,b,b9) & parallelogram (a,a9,c,c9) implies parallelogram (b,b9,c,c9)

    proof

      assume that

       A1: (a,b,c) are_collinear and

       A2: b <> c and

       A3: parallelogram (a,a9,b,b9) and

       A4: parallelogram (a,a9,c,c9);



       A5: b <> b9 by A3, Th36;

      (a,b) // (a,c) by A1;

      then

       A6: (a,b) // (b,c) by Th7;

      thus thesis by A2, A3, A4, A6, A5, Th23, Th50;

    end;

    theorem :: SEMI_AF1:52



     Th52: parallelogram (a,a9,b,b9) & parallelogram (a,a9,c,c9) & parallelogram (b,b9,d,d9) implies (c,d) // (c9,d9)

    proof

      assume that

       A1: parallelogram (a,a9,b,b9) and

       A2: parallelogram (a,a9,c,c9) and

       A3: parallelogram (b,b9,d,d9);

       A4:

      now

        assume

         A5: not (a,a9,d) are_collinear ;

         parallelogram (b,b9,a,a9) by A1, Th43;

        then parallelogram (a,a9,d,d9) by A3, A5, Th50;

        hence thesis by A2, Th49;

      end;

       A6:

      now



         A7: ( not (a,a9,b) are_collinear ) & (a,a9) // (a,a9) by A1, Th1;



         A8: a <> a9 by A1, Th36;

        assume that

         A9: (b,b9,c) are_collinear and

         A10: (a,a9,d) are_collinear ;

        a <> b by A1, Th36;

        then

        consider x such that

         A11: (a,b,x) are_collinear and

         A12: x <> a and

         A13: x <> b by Th48;

        (a,b) // (a,x) by A11;

        then

        consider y such that

         A14: parallelogram (a,a9,x,y) by A12, A7, A8, Th23, Th44;



         A15: not (x,y,d) are_collinear by A10, A14, Th39;

         parallelogram (b,b9,x,y) by A1, A11, A13, A14, Th51;

        then

         A16: parallelogram (x,y,d,d9) by A3, A15, Th50;

         not (x,y,c) are_collinear by A1, A9, A11, A13, A14, Th39, Th51;

        then parallelogram (x,y,c,c9) by A2, A14, Th50;

        hence thesis by A16, Th49;

      end;

      now

        assume not (b,b9,c) are_collinear ;

        then parallelogram (b,b9,c,c9) by A1, A2, Th50;

        hence thesis by A3, Th49;

      end;

      hence thesis by A4, A6;

    end;



     Lm1: a <> b implies ex c, d st parallelogram (a,b,c,d)

    proof

      assume a <> b;

      then

      consider c such that

       A1: not (a,b,c) are_collinear by Th25;

      ex d st parallelogram (a,b,c,d) by A1, Th44;

      hence thesis;

    end;

    theorem :: SEMI_AF1:53

    a <> d implies ex b, c st parallelogram (a,b,c,d)

    proof

      assume a <> d;

      then

      consider b such that

       A1: not (a,d,b) are_collinear by Th25;

       not (b,a,d) are_collinear by A1, Th22;

      then

      consider c such that

       A2: parallelogram (b,a,d,c) by Th44;

       parallelogram (a,b,c,d) by A2, Th43;

      hence thesis;

    end;

    definition

      let SAS, a, b, r, s;

      :: SEMI_AF1:def4

      pred congr a,b,r,s means a = b & r = s or ex p, q st parallelogram (p,q,a,b) & parallelogram (p,q,r,s);

    end

    theorem :: SEMI_AF1:54



     Th54: congr (a,a,b,c) implies b = c by Th36;

    theorem :: SEMI_AF1:55



     Th55: congr (a,b,c,c) implies a = b by Th36;

    theorem :: SEMI_AF1:56



     Th56: congr (a,b,b,a) implies a = b by Th47;

    theorem :: SEMI_AF1:57



     Th57: congr (a,b,c,d) implies (a,b) // (c,d)

    proof

      assume

       A1: congr (a,b,c,d);

      now

        assume a <> b;

        then

        consider p, q such that

         A2: parallelogram (p,q,a,b) and

         A3: parallelogram (p,q,c,d) by A1;



         A4: (p,q) // (c,d) by A3;

        p <> q & (p,q) // (a,b) by A2, Th36;

        hence thesis by A4, Def1;

      end;

      hence thesis by Th3;

    end;

    theorem :: SEMI_AF1:58



     Th58: congr (a,b,c,d) implies (a,c) // (b,d)

    proof

      assume

       A1: congr (a,b,c,d);

      then

       A2: a <> b implies thesis by Th49;

      now

        assume

         A3: a = b;

        then c = d by A1, Th54;

        hence thesis by A3, Th1;

      end;

      hence thesis by A2;

    end;

    theorem :: SEMI_AF1:59



     Th59: congr (a,b,c,d) & not (a,b,c) are_collinear implies parallelogram (a,b,c,d) by Th57, Th58;

    theorem :: SEMI_AF1:60



     Th60: parallelogram (a,b,c,d) implies congr (a,b,c,d)

    proof



       A1: (a,b) // (a,b) by Th1;

      assume

       A2: parallelogram (a,b,c,d);

      then

       A3: ( not (a,c,b) are_collinear ) & a <> b by Th36, Th38;

      a <> c by A2, Th36;

      then

      consider p such that

       A4: (a,c,p) are_collinear and

       A5: a <> p and

       A6: c <> p by Th48;

      (a,c) // (a,p) by A4;

      then

      consider q such that

       A7: parallelogram (a,p,b,q) by A5, A1, A3, Th23, Th44;

       parallelogram (a,b,p,q) by A7, Th43;

      then parallelogram (c,d,p,q) by A2, A4, A6, Th51;

      then

       A8: parallelogram (p,q,c,d) by Th43;

       parallelogram (p,q,a,b) by A7, Th43;

      hence thesis by A8;

    end;

    theorem :: SEMI_AF1:61



     Th61: congr (a,b,c,d) & (a,b,c) are_collinear & parallelogram (r,s,a,b) implies parallelogram (r,s,c,d)

    proof

      assume that

       A1: congr (a,b,c,d) and

       A2: (a,b,c) are_collinear and

       A3: parallelogram (r,s,a,b);

      now



         A4: parallelogram (a,b,r,s) by A3, Th43;

        assume

         A5: a <> b;

        then

        consider p, q such that

         A6: parallelogram (p,q,a,b) and

         A7: parallelogram (p,q,c,d) by A1;

         parallelogram (a,b,p,q) by A6, Th43;

        then

         A8: (r,c) // (s,d) by A7, A4, Th52;

        (r,s) // (a,b) & (a,b) // (c,d) by A1, A3, Th57;

        then

         A9: (r,s) // (c,d) by A5, Th8;

         not (r,s,c) are_collinear by A2, A3, Th39;

        hence thesis by A9, A8;

      end;

      hence thesis by A3, Th36;

    end;

    theorem :: SEMI_AF1:62



     Th62: congr (a,b,c,x) & congr (a,b,c,y) implies x = y

    proof

      assume that

       A1: congr (a,b,c,x) and

       A2: congr (a,b,c,y);

       A3:

      now

        assume that a <> b and

         A4: not (a,b,c) are_collinear ;

         parallelogram (a,b,c,x) & parallelogram (a,b,c,y) by A1, A2, A4, Th59;

        hence thesis by Th45;

      end;

       A5:

      now

        assume that

         A6: a <> b and

         A7: (a,b,c) are_collinear ;

        consider p, q such that

         A8: parallelogram (a,b,p,q) by A6, Lm1;

         parallelogram (p,q,a,b) by A8, Th43;

        then parallelogram (p,q,c,x) & parallelogram (p,q,c,y) by A1, A2, A7, Th61;

        hence thesis by Th45;

      end;

      now

        assume

         A9: a = b;

        then c = x by A1, Th54;

        hence thesis by A2, A9, Th54;

      end;

      hence thesis by A5, A3;

    end;

    theorem :: SEMI_AF1:63



     Th63: ex d st congr (a,b,c,d)

    proof

       A1:

      now

        assume a = b;

        then congr (a,b,c,c);

        hence thesis;

      end;

       A2:

      now

        assume that

         A3: a <> b and

         A4: (a,b,c) are_collinear ;

        consider p, q such that

         A5: parallelogram (a,b,p,q) by A3, Lm1;

         not (p,q,c) are_collinear by A4, A5, Th39;

        then

        consider d such that

         A6: parallelogram (p,q,c,d) by Th44;

         parallelogram (p,q,a,b) by A5, Th43;

        then congr (a,b,c,d) by A6;

        hence thesis;

      end;

      now

        assume that a <> b and

         A7: not (a,b,c) are_collinear ;

        ex d st parallelogram (a,b,c,d) by A7, Th44;

        hence thesis by Th60;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: SEMI_AF1:64



     Th64: congr (a,b,a,b)

    proof

      now

        assume a <> b;

        then

        consider p, q such that

         A1: parallelogram (a,b,p,q) by Lm1;

         parallelogram (p,q,a,b) by A1, Th43;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: SEMI_AF1:65



     Th65: congr (r,s,a,b) & congr (r,s,c,d) implies congr (a,b,c,d)

    proof

      assume that

       A1: congr (r,s,a,b) and

       A2: congr (r,s,c,d);

       A3:

      now

        assume that r <> s and

         A4: ( not (r,s,a) are_collinear ) & not (r,s,c) are_collinear ;

         parallelogram (r,s,a,b) & parallelogram (r,s,c,d) by A1, A2, A4, Th59;

        hence thesis;

      end;

       A5:

      now

        assume that

         A6: r <> s and

         A7: (r,s,c) are_collinear ;

        consider p, q such that

         A8: parallelogram (p,q,r,s) and

         A9: parallelogram (p,q,a,b) by A1, A6;

         parallelogram (p,q,c,d) by A2, A7, A8, Th61;

        hence thesis by A9;

      end;

       A10:

      now

        assume that

         A11: r <> s and

         A12: (r,s,a) are_collinear ;

        consider p, q such that

         A13: parallelogram (p,q,r,s) and

         A14: parallelogram (p,q,c,d) by A2, A11;

         parallelogram (p,q,a,b) by A1, A12, A13, Th61;

        hence thesis by A14;

      end;

      r = s implies thesis by A1, A2, Th54;

      hence thesis by A10, A5, A3;

    end;

    theorem :: SEMI_AF1:66

     congr (a,b,c,d) implies congr (c,d,a,b);

    theorem :: SEMI_AF1:67



     Th67: congr (a,b,c,d) implies congr (b,a,d,c)

    proof

      assume

       A1: congr (a,b,c,d);

       A2:

      now

        assume a <> b;

        then

        consider p, q such that

         A3: parallelogram (p,q,a,b) & parallelogram (p,q,c,d) by A1;

         parallelogram (q,p,b,a) & parallelogram (q,p,d,c) by A3, Th43;

        hence thesis;

      end;

      a = b implies thesis by A1, Th54;

      hence thesis by A2;

    end;

    theorem :: SEMI_AF1:68



     Th68: congr (a,b,c,d) implies congr (a,c,b,d)

    proof

      assume

       A1: congr (a,b,c,d);

       A2:

      now

        assume

         A3: a = c;

         congr (a,b,a,b) by Th64;

        then b = d by A1, A3, Th62;

        hence thesis by A3;

      end;

       A4:

      now

        assume that

         A5: a <> b and

         A6: a <> c and

         A7: (a,b,c) are_collinear ;



         A8: (a,b) // (a,c) by A7;

        consider p, q such that

         A9: parallelogram (p,q,a,b) and

         A10: parallelogram (p,q,c,d) by A1, A5;



         A11: (a,p) // (a,p) by Th1;

        ( not (a,b,p) are_collinear ) & a <> p by A9, Th36, Th38;

        then

        consider r such that

         A12: parallelogram (a,c,p,r) by A6, A8, A11, Th23, Th44;



         A13: (a,c) // (p,r) by A12;



         A14: (p,q) // (c,d) by A10;

        p <> q & (p,q) // (a,b) by A9, Th36;

        then

         A15: (a,b) // (c,d) by A14, Def1;

        then (a,c) // (b,d) by A5, A7, Th32;

        then

         A16: (p,r) // (b,d) by A6, A13, Def1;

         parallelogram (p,r,a,c) by A12, Th43;

        then

         A17: (p,a) // (r,c);

        (p,a) // (q,b) & p <> a by A9, Th36;

        then

         A18: (r,c) // (q,b) by A17, Def1;

        (p,c) // (q,d) by A10;

        then

         A19: (q,d) // (p,c) by Th6;

        (p,q) // (a,b) by A9;

        then

         A20: (a,b) // (p,q) by Th6;



         A21: (a,c) // (p,r) by A12;

        (a,b) // (a,c) by A7;

        then (a,c) // (p,q) by A5, A20, Def1;

        then (p,q) // (p,r) by A6, A21, Def1;

        then

         A22: (r,q) // (r,p) by Th7;

        (a,c,b) are_collinear by A7, Th22;

        then

         A23: not (p,r,b) are_collinear by A12, Th39;



         A24: parallelogram (p,r,a,c) by A12, Th43;

        (c,b) // (c,d) by A5, A7, A15, Th33;

        then (b,c) // (b,d) by Th7;

        then (p,b) // (r,d) by A22, A18, A19, Def1;

        then parallelogram (p,r,b,d) by A23, A16;

        hence thesis by A24;

      end;

       A25:

      now

        assume that a <> b and a <> c and

         A26: not (a,b,c) are_collinear ;

         parallelogram (a,b,c,d) by A1, A26, Th59;

        then parallelogram (a,c,b,d) by Th43;

        hence thesis by Th60;

      end;

      now

        assume

         A27: a = b;

        then c = d by A1, Th54;

        hence thesis by A27, Th64;

      end;

      hence thesis by A2, A4, A25;

    end;

    theorem :: SEMI_AF1:69



     Th69: congr (a,b,c,d) implies congr (c,d,a,b) & congr (b,a,d,c) & congr (a,c,b,d) & congr (d,c,b,a) & congr (b,d,a,c) & congr (c,a,d,b) & congr (d,b,c,a)

    proof

      assume

       A1: congr (a,b,c,d);

      then congr (c,d,a,b);

      then

       A2: congr (d,c,b,a) by Th67;

       congr (b,a,d,c) & congr (a,c,b,d) by A1, Th67, Th68;

      hence thesis by A2, Th67, Th68;

    end;

    theorem :: SEMI_AF1:70



     Th70: congr (a,b,p,q) & congr (b,c,q,s) implies congr (a,c,p,s)

    proof

      assume congr (a,b,p,q) & congr (b,c,q,s);

      then congr (b,q,a,p) & congr (b,q,c,s) by Th69;

      then congr (a,p,c,s) by Th65;

      hence thesis by Th68;

    end;

    theorem :: SEMI_AF1:71



     Th71: congr (b,a,p,q) & congr (c,a,p,r) implies congr (b,c,r,q)

    proof

      assume that

       A1: congr (b,a,p,q) and

       A2: congr (c,a,p,r);



       A3: congr (r,p,a,c) by A2, Th69;

      consider s such that

       A4: congr (p,q,r,s) by Th63;

       congr (r,p,s,q) by A4, Th69;

      then

       A5: congr (a,c,s,q) by A3, Th65;

       congr (p,q,b,a) by A1;

      then congr (b,a,r,s) by A4, Th65;

      hence thesis by A5, Th70;

    end;

    theorem :: SEMI_AF1:72

     congr (a,o,o,p) & congr (b,o,o,q) implies congr (a,b,q,p) by Th71;

    theorem :: SEMI_AF1:73



     Th73: congr (b,a,p,q) & congr (c,a,p,r) implies (b,c) // (q,r)

    proof

      assume congr (b,a,p,q) & congr (c,a,p,r);

      then congr (b,c,r,q) by Th71;

      then (b,c) // (r,q) by Th57;

      hence thesis by Th6;

    end;

    theorem :: SEMI_AF1:74

     congr (a,o,o,p) & congr (b,o,o,q) implies (a,b) // (p,q) by Th73;

    definition

      let SAS, a, b, o;

      :: SEMI_AF1:def5

      func sum (a,b,o) -> Element of SAS means

      : Def5: congr (o,a,b,it );

      correctness by Th62, Th63;

    end

    definition

      let SAS, a, o;

      :: SEMI_AF1:def6

      func opposite (a,o) -> Element of SAS means

      : Def6: ( sum (a,it ,o)) = o;

      existence

      proof

        consider b be Element of SAS such that

         A1: congr (a,o,o,b) by Th63;

        take b;

         congr (o,a,b,o) by A1, Th67;

        hence thesis by Def5;

      end;

      uniqueness

      proof

        let b1,b2 be Element of SAS such that

         A2: ( sum (a,b1,o)) = o and

         A3: ( sum (a,b2,o)) = o;

         congr (o,a,b2,o) by A3, Def5;

        then

         A4: congr (a,o,o,b2) by Th67;

         congr (o,a,b1,o) by A2, Def5;

        then congr (a,o,o,b1) by Th67;

        hence thesis by A4, Th62;

      end;

    end

    definition

      let SAS, a, b, o;

      :: SEMI_AF1:def7

      func diff (a,b,o) -> Element of SAS equals ( sum (a,( opposite (b,o)),o));

      correctness ;

    end

    theorem :: SEMI_AF1:75



     Th75: ( sum (a,o,o)) = a by Th64, Def5;

    theorem :: SEMI_AF1:76

    ex x st ( sum (a,x,o)) = o

    proof

      consider x such that

       A1: congr (a,o,o,x) by Th63;



       A2: congr (o,a,x,( sum (a,x,o))) by Def5;

       congr (o,a,x,o) by A1, Th69;

      hence thesis by A2, Th62;

    end;

    theorem :: SEMI_AF1:77

    ( sum (( sum (a,b,o)),c,o)) = ( sum (a,( sum (b,c,o)),o))

    proof

       congr (o,a,b,( sum (a,b,o))) & congr (o,a,( sum (b,c,o)),( sum (a,( sum (b,c,o)),o))) by Def5;

      then

       A1: congr (b,( sum (a,b,o)),( sum (b,c,o)),( sum (a,( sum (b,c,o)),o))) by Th65;

       congr (o,b,c,( sum (b,c,o))) by Def5;

      then

       A2: congr (b,o,( sum (b,c,o)),c) by Th69;

       congr (o,( sum (a,b,o)),c,( sum (( sum (a,b,o)),c,o))) by Def5;

      then congr (b,( sum (a,b,o)),( sum (b,c,o)),( sum (( sum (a,b,o)),c,o))) by A2, Th70;

      hence thesis by A1, Th62;

    end;

    theorem :: SEMI_AF1:78



     Th78: ( sum (a,b,o)) = ( sum (b,a,o))

    proof

       congr (o,b,a,( sum (b,a,o))) by Def5;

      then congr (o,a,b,( sum (b,a,o))) by Th69;

      hence thesis by Def5;

    end;

    theorem :: SEMI_AF1:79

    ( sum (a,a,o)) = o implies a = o

    proof

      assume ( sum (a,a,o)) = o;

      then congr (o,a,a,o) by Def5;

      hence thesis by Th56;

    end;

    theorem :: SEMI_AF1:80

    ( sum (a,x,o)) = ( sum (a,y,o)) implies x = y

    proof

      assume

       A1: ( sum (a,x,o)) = ( sum (a,y,o));

       congr (o,a,x,( sum (a,x,o))) by Def5;

      then

       A2: congr (a,o,( sum (a,x,o)),x) by Th69;

       congr (o,a,y,( sum (a,y,o))) by Def5;

      then congr (a,o,( sum (a,x,o)),y) by A1, Th69;

      hence thesis by A2, Th62;

    end;

    theorem :: SEMI_AF1:81



     Th81: congr (a,o,o,( opposite (a,o)))

    proof

      ( sum (a,( opposite (a,o)),o)) = o & congr (o,a,( opposite (a,o)),( sum (a,( opposite (a,o)),o))) by Def5, Def6;

      hence thesis by Th69;

    end;

    theorem :: SEMI_AF1:82



     Th82: ( opposite (a,o)) = ( opposite (b,o)) implies a = b

    proof

      assume

       A1: ( opposite (a,o)) = ( opposite (b,o));

       congr (a,o,o,( opposite (a,o))) by Th81;

      then

       A2: congr (( opposite (a,o)),o,o,a) by Th69;

       congr (b,o,o,( opposite (b,o))) by Th81;

      then congr (( opposite (a,o)),o,o,b) by A1, Th69;

      hence thesis by A2, Th62;

    end;

    theorem :: SEMI_AF1:83

    (a,b) // (( opposite (a,o)),( opposite (b,o)))

    proof

      ( sum (b,( opposite (b,o)),o)) = o by Def6;

      then congr (o,b,( opposite (b,o)),o) by Def5;

      then

       A1: congr (b,o,o,( opposite (b,o))) by Th69;

      ( sum (a,( opposite (a,o)),o)) = o by Def6;

      then congr (o,a,( opposite (a,o)),o) by Def5;

      then congr (a,o,o,( opposite (a,o))) by Th69;

      hence thesis by A1, Th73;

    end;

    theorem :: SEMI_AF1:84

    ( opposite (o,o)) = o

    proof

      ( sum (o,( opposite (o,o)),o)) = o by Def6;

      then ( sum (( opposite (o,o)),o,o)) = o by Th78;

      hence thesis by Th75;

    end;

    theorem :: SEMI_AF1:85



     Th85: (p,q) // (( sum (p,r,o)),( sum (q,r,o)))

    proof

       congr (o,p,r,( sum (p,r,o))) by Def5;

      then

       A1: congr (p,o,( sum (p,r,o)),r) by Th69;

       congr (o,q,r,( sum (q,r,o))) by Def5;

      then congr (p,q,( sum (p,r,o)),( sum (q,r,o))) by A1, Th70;

      hence thesis by Th57;

    end;

    theorem :: SEMI_AF1:86

    (p,q) // (r,s) implies (p,q) // (( sum (p,r,o)),( sum (q,s,o)))

    proof

      assume

       A1: (p,q) // (r,s);

      now

        consider t such that

         A2: congr (o,q,r,t) by Th63;

        assume that

         A3: p <> q and

         A4: r <> s;

         congr (o,q,s,( sum (q,s,o))) by Def5;

        then congr (r,t,s,( sum (q,s,o))) by A2, Th65;

        then

         A5: congr (r,s,t,( sum (q,s,o))) by Th69;

        then

         A6: t <> ( sum (q,s,o)) by A4, Th55;

        (r,s) // (t,( sum (q,s,o))) by A5, Th57;

        then

         A7: (p,q) // (t,( sum (q,s,o))) by A1, A4, Th8;

         congr (o,p,r,( sum (p,r,o))) by Def5;

        then congr (p,o,( sum (p,r,o)),r) by Th69;

        then congr (p,q,( sum (p,r,o)),t) by A2, Th70;

        then (p,q) // (( sum (p,r,o)),t) by Th57;

        then (p,q) // (t,( sum (p,r,o))) by Th6;

        then (t,( sum (q,s,o))) // (t,( sum (p,r,o))) by A3, A7, Def1;

        then (t,( sum (q,s,o))) // (( sum (p,r,o)),( sum (q,s,o))) by Th7;

        hence thesis by A6, A7, Th8;

      end;

      hence thesis by Th3, Th85;

    end;

    theorem :: SEMI_AF1:87



     Th87: ( diff (a,b,o)) = o iff a = b

    proof

      ( diff (a,b,o)) = o implies a = b

      proof

        assume ( diff (a,b,o)) = o;

        then ( opposite (a,o)) = ( opposite (b,o)) by Def6;

        hence thesis by Th82;

      end;

      hence thesis by Def6;

    end;

    theorem :: SEMI_AF1:88



     Th88: (o,( diff (b,a,o))) // (a,b)

    proof

       congr (a,o,o,( opposite (a,o))) by Th81;

      then

       A1: congr (o,( opposite (a,o)),a,o);

       congr (o,b,( opposite (a,o)),( sum (b,( opposite (a,o)),o))) by Def5;

      then congr (o,( opposite (a,o)),b,( diff (b,a,o))) by Th69;

      then congr (a,o,b,( diff (b,a,o))) by A1, Th65;

      then congr (o,( diff (b,a,o)),a,b) by Th69;

      hence thesis by Th57;

    end;

    theorem :: SEMI_AF1:89

    (o,( diff (b,a,o)),( diff (d,c,o))) are_collinear iff (a,b) // (c,d)

    proof



       A1: (a,b) // (c,d) implies (o,( diff (b,a,o)),( diff (d,c,o))) are_collinear

      proof

        assume

         A2: (a,b) // (c,d);

         A3:

        now

          (o,( diff (d,c,o))) // (c,d) by Th88;

          then

           A4: (c,d) // (o,( diff (d,c,o))) by Th6;

          assume that

           A5: a <> b and

           A6: c <> d;

          (o,( diff (b,a,o))) // (a,b) by Th88;

          then (a,b) // (o,( diff (b,a,o))) by Th6;

          then (o,( diff (b,a,o))) // (c,d) by A2, A5, Def1;

          then (o,( diff (b,a,o))) // (o,( diff (d,c,o))) by A6, A4, Th8;

          hence thesis;

        end;

        now

          assume a = b or c = d;

          then o = ( diff (b,a,o)) or o = ( diff (d,c,o)) by Th87;

          then (o,( diff (b,a,o))) // (o,( diff (d,c,o))) by Def1, Th3;

          hence thesis;

        end;

        hence thesis by A3;

      end;

      (o,( diff (b,a,o)),( diff (d,c,o))) are_collinear implies (a,b) // (c,d)

      proof

        assume

         A7: (o,( diff (b,a,o)),( diff (d,c,o))) are_collinear ;

         A8:

        now



           A9: (o,( diff (d,c,o))) // (c,d) by Th88;

          assume that

           A10: o <> ( diff (b,a,o)) and

           A11: o <> ( diff (d,c,o));

          (o,( diff (b,a,o))) // (o,( diff (d,c,o))) & (o,( diff (b,a,o))) // (a,b) by A7, Th88;

          then (o,( diff (d,c,o))) // (a,b) by A10, Def1;

          hence thesis by A11, A9, Def1;

        end;

        now

          assume o = ( diff (b,a,o)) or o = ( diff (d,c,o));

          then a = b or c = d by Th87;

          hence thesis by Def1, Th3;

        end;

        hence thesis by A8;

      end;

      hence thesis by A1;

    end;

    definition

      let SAS, a, b, c, d, o;

      :: SEMI_AF1:def8

      pred trap a,b,c,d,o means not (o,a,c) are_collinear & (o,a,b) are_collinear & (o,c,d) are_collinear & (a,c) // (b,d);

    end

    definition

      let SAS, o, p;

      :: SEMI_AF1:def9

      pred qtrap o,p means for b, c holds ex d st ((o,p,b) are_collinear implies (o,c,d) are_collinear & (p,c) // (b,d));

    end

    theorem :: SEMI_AF1:90



     Th90: trap (a,b,c,d,o) implies o <> a & a <> c & c <> o by Th24;

    theorem :: SEMI_AF1:91

     trap (a,b,c,x,o) & trap (a,b,c,y,o) implies x = y by Th34;

    theorem :: SEMI_AF1:92

     not (o,a,b) are_collinear implies trap (a,o,b,o,o) by Def1, Th24;

    theorem :: SEMI_AF1:93



     Th93: trap (a,b,c,d,o) implies trap (c,d,a,b,o) by Th22, Th6;

    theorem :: SEMI_AF1:94



     Th94: trap (a,b,c,d,d) implies d = b

    proof

      assume

       A1: trap (a,b,c,d,d);

      then (a,c) // (b,d);

      then

       A2: (d,b) // (a,c) by Th6;

      (d,a,b) are_collinear by A1;

      then (d,a) // (d,b);

      then

       A3: (d,b) // (a,d) by Th6;

      assume not thesis;

      then (a,d) // (a,c) by A3, A2, Def1;

      then

       A4: (d,a) // (d,c) by Th7;

       not (d,a,c) are_collinear by A1;

      hence contradiction by A4;

    end;

    theorem :: SEMI_AF1:95



     Th95: o <> b & trap (a,b,c,d,o) implies not (o,b,d) are_collinear

    proof

      assume that

       A1: o <> b and

       A2: trap (a,b,c,d,o);

      (o,a,b) are_collinear by A2;

      then

       A3: (o,a) // (o,b);

      (o,c,d) are_collinear by A2;

      then

       A4: (o,c) // (o,d);

      o <> d & not (o,a,c) are_collinear by A1, A2, Th94;

      hence thesis by A1, A3, A4, Th23;

    end;

    theorem :: SEMI_AF1:96

    o <> b & trap (a,b,c,d,o) implies trap (b,a,d,c,o) by Th22, Th6, Th95;

    theorem :: SEMI_AF1:97

     trap (a,b,c,d,b) implies b = d by Th93, Th94;

    theorem :: SEMI_AF1:98



     Th98: trap (a,p,b,q,o) & trap (a,p,c,r,o) implies (b,c) // (q,r)

    proof

      assume that

       A1: trap (a,p,b,q,o) and

       A2: trap (a,p,c,r,o);

       not (o,a,b) are_collinear by A1;

      then

       A3: not (o,a) // (o,b);

      (o,c,r) are_collinear by A2;

      then

       A4: (o,c) // (o,r);

       not (o,a,c) are_collinear by A2;

      then

       A5: not (o,a) // (o,c);

      (o,b,q) are_collinear by A1;

      then

       A6: (o,b) // (o,q);

      (o,a,p) are_collinear by A1;

      then

       A7: (o,a) // (o,p);

      (a,b) // (p,q) & (a,c) // (p,r) by A1, A2;

      hence thesis by A3, A7, A6, A5, A4, Def1;

    end;

    theorem :: SEMI_AF1:99



     Th99: trap (a,p,b,q,o) & trap (a,p,c,r,o) & not (o,b,c) are_collinear implies trap (b,q,c,r,o) by Th98;

    theorem :: SEMI_AF1:100

     trap (a,p,b,q,o) & trap (a,p,c,r,o) & trap (b,q,d,s,o) implies (c,d) // (r,s)

    proof

      assume that

       A1: trap (a,p,b,q,o) and

       A2: trap (a,p,c,r,o) and

       A3: trap (b,q,d,s,o);

       A4:

      now

        assume

         A5: not (o,a,d) are_collinear ;

         trap (b,q,a,p,o) by A1, Th93;

        then trap (a,p,d,s,o) by A3, A5, Th99;

        hence thesis by A2, Th98;

      end;

       A6:

      now

         not (o,a,b) are_collinear by A1;

        then not (b,a,o) are_collinear by Th22;

        then

        consider x such that

         A7: parallelogram (b,a,o,x) by Th44;

        (o,b,q) are_collinear by A1;

        then (o,b) // (o,q);

        then

         A8: (b,o) // (q,o) by Th6;



         A9: (o,x) // (o,x) by Th1;

        (b,o) // (a,x) & b <> o by A7, Th36;

        then

         A10: (q,o) // (a,x) by A8, Def1;



         A11: not (o,x,b) are_collinear by A7, Th38;



         A12: o <> d by A3, Th90;

        assume that

         A13: o <> p and

         A14: (o,b,c) are_collinear and

         A15: (o,a,d) are_collinear ;

         not (o,p,q) are_collinear by A1, A13, Th95;

        then not (q,p,o) are_collinear by Th22;

        then

        consider y such that

         A16: parallelogram (q,p,o,y) by Th44;



         A17: not (o,x,a) are_collinear by A7, Th38;



         A18: o <> c by A2, Th90;

        (a,b) // (p,q) by A1;

        then

         A19: (b,a) // (q,p) by Th6;



         A20: (o,a,p) are_collinear by A1;

        (b,a) // (o,x) & b <> a by A7, Th36;

        then

         A21: (q,p) // (o,x) by A19, Def1;



         A22: o <> x by A7, Th36;

        q <> p & (q,p) // (o,y) by A16, Th36;

        then (o,x) // (o,y) by A21, Def1;

        then

         A23: (o,x,y) are_collinear ;

        (q,o) // (p,y) & q <> o by A16, Th36;

        then

         A24: (a,x) // (p,y) by A10, Def1;

         not (o,a,x) are_collinear by A7, Th38;

        then

         A25: trap (a,p,x,y,o) by A23, A24, A20;

         not (o,b,x) are_collinear by A7, Th38;

        then

         A26: trap (b,q,x,y,o) by A1, A25, Th99;

        (o,a) // (o,d) by A15;

        then

         A27: trap (x,y,d,s,o) by A3, A26, A22, A12, A17, A9, Th23, Th99;

        (o,b) // (o,c) by A14;

        then trap (x,y,c,r,o) by A2, A25, A11, A22, A18, A9, Th23, Th99;

        hence thesis by A27, Th98;

      end;

       A28:

      now

        assume

         A29: o = p;

        then o = q by A1, Th93, Th94;

        then

         A30: o = s by A3, Th93, Th94;

        o = r by A2, A29, Th93, Th94;

        hence thesis by A30, Def1;

      end;

      now

        assume not (o,b,c) are_collinear ;

        then trap (b,q,c,r,o) by A1, A2, Th99;

        hence thesis by A3, Th98;

      end;

      hence thesis by A4, A28, A6;

    end;

    theorem :: SEMI_AF1:101



     Th101: for o, a holds ex p st (o,a,p) are_collinear & qtrap (o,p)

    proof

      let o, a;

      consider p such that

       A1: for b, c holds (o,a) // (o,p) & ex d st (o,p) // (o,b) implies (o,c) // (o,d) & (p,c) // (b,d) by Def1;

      take p;

      now

        thus (o,a,p) are_collinear by A1;

        let b, c;

        consider d such that

         A2: (o,p) // (o,b) implies (o,c) // (o,d) & (p,c) // (b,d) by A1;

        take d;

        assume (o,p,b) are_collinear ;

        hence (o,c,d) are_collinear & (p,c) // (b,d) by A2;

      end;

      hence thesis;

    end;

    theorem :: SEMI_AF1:102



     Th102: ex x, y, z st x <> y & y <> z & z <> x

    proof

      consider x, y, z such that

       A1: not (x,y) // (x,z) by Def1;

      take x, y, z;

      thus thesis by A1, Def1, Th1, Th3;

    end;

    theorem :: SEMI_AF1:103



     Th103: qtrap (o,p) implies o <> p

    proof

      ex b st o <> b

      proof

        consider x, y, z such that

         A1: x <> y and y <> z and z <> x by Th102;

        o <> x or o <> y or o <> z by A1;

        hence thesis;

      end;

      then

      consider b such that

       A2: o <> b;

      consider c such that

       A3: not (o,b) // (o,c) by A2, Th13;

      assume qtrap (o,p);

      then

      consider d such that

       A4: (o,p,b) are_collinear implies (o,c,d) are_collinear & (p,c) // (b,d);

       A5:

      now

        assume that

         A6: b <> d & not (o,b) // (o,c) and

         A7: (o,d) // (b,d) and

         A8: (o,c) // (b,d);

        (d,o) // (d,b) by A7, Th6;

        hence b <> d & not (o,b) // (o,c) & (b,d) // (o,b) & (b,d) // (o,c) by A6, A8, Th6, Th7;

      end;

      assume not thesis;

      then (o,o) // (o,b) implies (o,c) // (o,d) & (o,c) // (b,d) by A4;

      then b = d & not (o,b) // (o,c) & (o,c) // (o,d) or b <> d & o <> c & not (o,b) // (o,c) & (o,c) // (o,d) & (o,c) // (b,d) by A3, Def1, Th3;

      hence contradiction by A5, Def1, Th6;

    end;

    theorem :: SEMI_AF1:104

     qtrap (o,p) implies ex q st not (o,p,q) are_collinear & qtrap (o,q)

    proof



       A1: (o,p) // (o,p) by Th1;

      assume

       A2: qtrap (o,p);

      then

       A3: o <> p by Th103;

      consider r such that

       A4: not (o,p,r) are_collinear by A2, Th25, Th103;

      consider q such that

       A5: (o,r,q) are_collinear and

       A6: qtrap (o,q) by Th101;

      take q;

      o <> q & (o,r) // (o,q) by A5, A6, Th103;

      hence thesis by A3, A4, A6, A1, Th23;

    end;

    theorem :: SEMI_AF1:105

     not (o,p,c) are_collinear & (o,p,b) are_collinear & qtrap (o,p) implies ex d st trap (p,b,c,d,o)

    proof

      assume that

       A1: ( not (o,p,c) are_collinear ) & (o,p,b) are_collinear and

       A2: qtrap (o,p);

      consider d such that

       A3: (o,p,b) are_collinear implies (o,c,d) are_collinear & (p,c) // (b,d) by A2;

      take d;

      thus thesis by A1, A3;

    end;