aff_1.miz

    begin

    reserve AS for AffinSpace;

    reserve a,a9,b,b9,c,d,o,p,q,r,s,x,y,z,t,u,w for Element of AS;

    definition

      let AS, a, b, c;

      :: AFF_1:def1

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

    end

    ::$Canceled

    theorem :: AFF_1:2



     Th1: (x,y) // (y,x) & (x,y) // (x,y) by DIRAF: 40;



     Lm1: (x,y) // (z,t) implies (z,t) // (x,y)

    proof

      assume

       A1: (x,y) // (z,t);

      now

        assume

         A2: x <> y;

        (x,y) // (x,y) by Th1;

        hence thesis by A1, A2, DIRAF: 40;

      end;

      hence thesis by DIRAF: 40;

    end;

    theorem :: AFF_1:3



     Th2: (x,y) // (z,z) & (z,z) // (x,y) by Lm1, DIRAF: 40;



     Lm2: (x,y) // (z,t) implies (y,x) // (z,t)

    proof

      assume

       A1: (x,y) // (z,t);

      (x,y) // (y,x) by Th1;

      then (y,x) // (z,t) or x = y by A1, DIRAF: 40;

      hence thesis by Th2;

    end;



     Lm3: (x,y) // (z,t) implies (x,y) // (t,z)

    proof

      assume (x,y) // (z,t);

      then (z,t) // (x,y) by Lm1;

      then (t,z) // (x,y) by Lm2;

      hence thesis by Lm1;

    end;

    theorem :: AFF_1:4



     Th3: (x,y) // (z,t) implies (x,y) // (t,z) & (y,x) // (z,t) & (y,x) // (t,z) & (z,t) // (x,y) & (z,t) // (y,x) & (t,z) // (x,y) & (t,z) // (y,x)

    proof

      assume

       A1: (x,y) // (z,t);

      hence (x,y) // (t,z) & (y,x) // (z,t) by Lm2, Lm3;

      hence (y,x) // (t,z) by Lm2;

      thus (z,t) // (x,y) by A1, Lm1;

      hence (z,t) // (y,x) & (t,z) // (x,y) by Lm2, Lm3;

      hence thesis by Lm3;

    end;

    theorem :: AFF_1:5



     Th4: a <> b & ((a,b) // (x,y) & (a,b) // (z,t) or (a,b) // (x,y) & (z,t) // (a,b) or (x,y) // (a,b) & (z,t) // (a,b) or (x,y) // (a,b) & (a,b) // (z,t)) implies (x,y) // (z,t)

    proof

      assume that

       A1: a <> b and

       A2: (a,b) // (x,y) & (a,b) // (z,t) or (a,b) // (x,y) & (z,t) // (a,b) or (x,y) // (a,b) & (z,t) // (a,b) or (x,y) // (a,b) & (a,b) // (z,t);



       A3: (a,b) // (z,t) by A2, Th3;

      (a,b) // (x,y) by A2, Th3;

      hence thesis by A1, A3, DIRAF: 40;

    end;



     Lm4: LIN (x,y,z) implies LIN (x,z,y) & LIN (y,x,z) by DIRAF: 40, Th3;

    theorem :: AFF_1:6



     Th5: LIN (x,y,z) implies LIN (x,z,y) & LIN (y,x,z) & LIN (y,z,x) & LIN (z,x,y) & LIN (z,y,x)

    proof

      assume LIN (x,y,z);

      hence LIN (x,z,y) & LIN (y,x,z) by Lm4;

      hence LIN (y,z,x) & LIN (z,x,y) by Lm4;

      hence thesis by Lm4;

    end;

    theorem :: AFF_1:7



     Th6: LIN (x,x,y) & LIN (x,y,y) & LIN (x,y,x) by Th1, Th2;

    theorem :: AFF_1:8



     Th7: x <> y & LIN (x,y,z) & LIN (x,y,t) & LIN (x,y,u) implies LIN (z,t,u)

    proof

      assume that

       A1: x <> y and

       A2: LIN (x,y,z) and

       A3: LIN (x,y,t) and

       A4: LIN (x,y,u);

       A5:

      now



         A6: (x,y) // (x,z) by A2;

        (x,y) // (x,u) by A4;

        then (x,z) // (x,u) by A1, A6, Th4;

        then

         A7: (z,x) // (z,u) by DIRAF: 40;

        (x,y) // (x,t) by A3;

        then (x,z) // (x,t) by A1, A6, Th4;

        then

         A8: (z,x) // (z,t) by DIRAF: 40;

        assume x <> z;

        then (z,t) // (z,u) by A8, A7, Th4;

        hence thesis;

      end;

      x = z implies thesis by A1, A3, A4, Th4;

      hence thesis by A5;

    end;

    theorem :: AFF_1:9



     Th8: x <> y & LIN (x,y,z) & (x,y) // (z,t) implies LIN (x,y,t)

    proof

      assume that

       A1: x <> y and

       A2: LIN (x,y,z) and

       A3: (x,y) // (z,t);

      now

        (x,y) // (x,z) by A2;

        then (x,z) // (z,t) by A1, A3, Th4;

        then (z,x) // (z,t) by Th3;

        then LIN (z,x,t);

        then

         A4: LIN (x,z,t) by Th5;

        assume

         A5: z <> x;



         A6: LIN (x,z,x) by Th6;

         LIN (x,z,y) by A2, Th5;

        hence thesis by A5, A4, A6, Th7;

      end;

      hence thesis by A3;

    end;

    theorem :: AFF_1:10



     Th9: LIN (x,y,z) & LIN (x,y,t) implies (x,y) // (z,t)

    proof

      assume that

       A1: LIN (x,y,z) and

       A2: LIN (x,y,t);

      now



         A3: (x,y) // (x,t) by A2;



         A4: (x,y) // (x,z) by A1;

        assume x <> y;

        then (x,z) // (x,t) by A4, A3, Th4;

        then (z,x) // (z,t) by DIRAF: 40;

        then (x,z) // (z,t) by Th3;

        hence thesis by A4, A3, Th4;

      end;

      hence thesis by Th2;

    end;

    theorem :: AFF_1:11



     Th10: u <> z & LIN (x,y,u) & LIN (x,y,z) & LIN (u,z,w) implies LIN (x,y,w)

    proof

      assume that

       A1: u <> z and

       A2: LIN (x,y,u) and

       A3: LIN (x,y,z) and

       A4: LIN (u,z,w);

      now

        assume

         A5: x <> y;

         LIN (x,y,x) by Th6;

        then

         A6: LIN (z,u,x) by A2, A3, A5, Th7;

         LIN (x,y,y) by Th6;

        then

         A7: LIN (z,u,y) by A2, A3, A5, Th7;

         LIN (z,u,w) by A4, Th5;

        hence thesis by A1, A7, A6, Th7;

      end;

      hence thesis by Th6;

    end;

    theorem :: AFF_1:12



     Th11: ex x, y, z st not LIN (x,y,z)

    proof

      consider x, y, z such that

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

       not LIN (x,y,z) by A1;

      hence thesis;

    end;

    theorem :: AFF_1:13

    x <> y implies ex z st not LIN (x,y,z)

    proof

      assume

       A1: x <> y;

      consider a, b, c such that

       A2: not LIN (a,b,c) by Th11;

      assume

       A3: not thesis;

      then

       A4: LIN (x,y,b);



       A5: LIN (x,y,c) by A3;

       LIN (x,y,a) by A3;

      hence contradiction by A1, A2, A4, A5, Th7;

    end;

    theorem :: AFF_1:14

     not LIN (o,a,b) & LIN (o,b,b9) & (a,b) // (a,b9) implies b = b9

    proof

      assume that

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

       A2: LIN (o,b,b9) and

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

       LIN (a,b,b9) by A3;

      then

       A4: LIN (b,b9,a) by Th5;



       A5: LIN (b,b9,b) by Th6;

      assume

       A6: b <> b9;

       LIN (b,b9,o) by A2, Th5;

      hence contradiction by A1, A6, A4, A5, Th7;

    end;

    definition

      let AS, a, b;

      :: AFF_1:def2

      func Line (a,b) -> Subset of AS means

      : Def2: for x holds x in it iff LIN (a,b,x);

      existence

      proof

        defpred P[ set] means for y st y = $1 holds LIN (a,b,y);

        consider X be Subset of AS such that

         A1: for x be set holds x in X iff x in the carrier of AS & P[x] from SUBSET_1:sch 1;

        take X;

        let x;

        thus x in X implies LIN (a,b,x) by A1;

        assume LIN (a,b,x);

        then for y st y = x holds LIN (a,b,y);

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of AS such that

         A2: for x holds x in X1 iff LIN (a,b,x) and

         A3: for x holds x in X2 iff LIN (a,b,x);

        for x be object holds x in X1 iff x in X2 by A2, A3;

        hence thesis by TARSKI: 2;

      end;

    end

    reserve A,C,D,K for Subset of AS;



     Lm5: ( Line (a,b)) c= ( Line (b,a))

    proof

      let x be object;

      assume

       A1: x in ( Line (a,b));

      then

      reconsider x9 = x as Element of AS;

       LIN (a,b,x9) by A1, Def2;

      then LIN (b,a,x9) by Th5;

      hence x in ( Line (b,a)) by Def2;

    end;

    definition

      let AS, a, b;

      :: original: Line

      redefine

      func Line (a,b);

      commutativity

      proof

        let a, b;



         A1: ( Line (b,a)) c= ( Line (a,b)) by Lm5;

        ( Line (a,b)) c= ( Line (b,a)) by Lm5;

        hence thesis by A1, XBOOLE_0:def 10;

      end;

    end

    theorem :: AFF_1:15



     Th14: a in ( Line (a,b)) & b in ( Line (a,b))

    proof



       A1: LIN (a,b,b) by Th6;

       LIN (a,b,a) by Th6;

      hence thesis by A1, Def2;

    end;

    theorem :: AFF_1:16



     Th15: c in ( Line (a,b)) & d in ( Line (a,b)) & c <> d implies ( Line (c,d)) c= ( Line (a,b))

    proof

      assume that

       A1: c in ( Line (a,b)) and

       A2: d in ( Line (a,b)) and

       A3: c <> d;



       A4: LIN (a,b,d) by A2, Def2;



       A5: LIN (a,b,c) by A1, Def2;

      let x be object;

      assume

       A6: x in ( Line (c,d));

      then

      reconsider x9 = x as Element of AS;

       LIN (c,d,x9) by A6, Def2;

      then LIN (a,b,x9) by A3, A5, A4, Th10;

      hence x in ( Line (a,b)) by Def2;

    end;

    theorem :: AFF_1:17



     Th16: c in ( Line (a,b)) & d in ( Line (a,b)) & a <> b implies ( Line (a,b)) c= ( Line (c,d))

    proof

      assume that

       A1: c in ( Line (a,b)) and

       A2: d in ( Line (a,b)) and

       A3: a <> b;



       A4: LIN (a,b,d) by A2, Def2;



       A5: LIN (a,b,c) by A1, Def2;

      let x be object;

      assume

       A6: x in ( Line (a,b));

      then

      reconsider x9 = x as Element of AS;

       LIN (a,b,x9) by A6, Def2;

      then LIN (c,d,x9) by A3, A5, A4, Th7;

      hence x in ( Line (c,d)) by Def2;

    end;

    definition

      let AS, A;

      :: AFF_1:def3

      attr A is being_line means

      : Def3: ex a, b st a <> b & A = ( Line (a,b));

    end

    registration

      let AS;

      cluster being_line for Subset of AS;

      existence

      proof

        set a = the Element of AS;

        consider b be Element of AS such that

         A1: a <> b by SUBSET_1: 50;

        take ( Line (a,b));

        thus thesis by A1;

      end;

    end



     Lm6: A is being_line & a in A & b in A & a <> b implies A = ( Line (a,b))

    proof

      assume that

       A1: A is being_line and

       A2: a in A and

       A3: b in A and

       A4: a <> b;



       A5: ex p, q st p <> q & A = ( Line (p,q)) by A1;

      then

       A6: A c= ( Line (a,b)) by A2, A3, Th16;

      ( Line (a,b)) c= A by A2, A3, A4, A5, Th15;

      hence thesis by A6, XBOOLE_0:def 10;

    end;

    theorem :: AFF_1:18



     Th17: A is being_line & C is being_line & a in A & b in A & a in C & b in C implies a = b or A = C

    proof

      assume that

       A1: A is being_line and

       A2: C is being_line and

       A3: a in A and

       A4: b in A and

       A5: a in C and

       A6: b in C;

      assume

       A7: a <> b;

      then A = ( Line (a,b)) by A1, A3, A4, Lm6;

      hence thesis by A2, A5, A6, A7, Lm6;

    end;

    theorem :: AFF_1:19



     Th18: A is being_line implies ex a, b st a in A & b in A & a <> b

    proof

      assume A is being_line;

      then

      consider a, b such that

       A1: a <> b and

       A2: A = ( Line (a,b));



       A3: b in A by A2, Th14;

      a in A by A2, Th14;

      hence thesis by A1, A3;

    end;

    theorem :: AFF_1:20



     Th19: A is being_line implies ex b st a <> b & b in A

    proof

      assume A is being_line;

      then

      consider p, q such that

       A1: p in A and

       A2: q in A and

       A3: p <> q by Th18;

      a = p implies a <> q & q in A by A2, A3;

      hence thesis by A1;

    end;

    theorem :: AFF_1:21



     Th20: LIN (a,b,c) iff ex A st A is being_line & a in A & b in A & c in A

    proof



       A1: LIN (a,b,c) implies ex A st A is being_line & a in A & b in A & c in A

      proof

        assume

         A2: LIN (a,b,c);

         A3:

        now

          set A = ( Line (a,b));



           A4: a in A by Th14;



           A5: b in A by Th14;

          assume a <> b;

          then

           A6: A is being_line;

          c in A by A2, Def2;

          hence thesis by A6, A4, A5;

        end;

         A7:

        now

          set A = ( Line (a,c));



           A8: c in A by Th14;

          assume a <> c;

          then

           A9: A is being_line;

           LIN (a,c,b) by A2, Th5;

          then

           A10: b in A by Def2;

          a in A by Th14;

          hence thesis by A9, A10, A8;

        end;

        now

          consider x such that

           A11: a <> x by SUBSET_1: 50;

          set A = ( Line (a,x));



           A12: a in A by Th14;

          assume that

           A13: a = b and

           A14: a = c;

          A is being_line by A11;

          hence thesis by A13, A14, A12;

        end;

        hence thesis by A3, A7;

      end;

      (ex A st A is being_line & a in A & b in A & c in A) implies LIN (a,b,c)

      proof

        given A such that

         A15: A is being_line and

         A16: a in A and

         A17: b in A and

         A18: c in A;

        consider p, q such that

         A19: p <> q and

         A20: A = ( Line (p,q)) by A15;



         A21: LIN (p,q,b) by A17, A20, Def2;



         A22: LIN (p,q,c) by A18, A20, Def2;

         LIN (p,q,a) by A16, A20, Def2;

        hence thesis by A19, A21, A22, Th7;

      end;

      hence thesis by A1;

    end;

    definition

      let AS, a, b, A;

      :: AFF_1:def4

      pred a,b // A means ex c, d st c <> d & A = ( Line (c,d)) & (a,b) // (c,d);

    end

    definition

      let AS, A, C;

      :: AFF_1:def5

      pred A // C means ex a, b st A = ( Line (a,b)) & a <> b & (a,b) // C;

    end

    theorem :: AFF_1:22



     Th21: c in ( Line (a,b)) & a <> b implies (d in ( Line (a,b)) iff (a,b) // (c,d))

    proof

      assume that

       A1: c in ( Line (a,b)) and

       A2: a <> b;



       A3: LIN (a,b,c) by A1, Def2;

      thus d in ( Line (a,b)) implies (a,b) // (c,d)

      proof

        assume d in ( Line (a,b));

        then LIN (a,b,d) by Def2;

        hence thesis by A3, Th9;

      end;

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

      then LIN (a,b,d) by A2, A3, Th8;

      hence thesis by Def2;

    end;

    theorem :: AFF_1:23



     Th22: A is being_line & a in A implies (b in A iff (a,b) // A)

    proof

      assume that

       A1: A is being_line and

       A2: a in A;

      consider p, q such that

       A3: p <> q and

       A4: A = ( Line (p,q)) by A1;

      hereby

        assume b in A;

        then (p,q) // (a,b) by A2, A3, A4, Th21;

        then (a,b) // (p,q) by Th3;

        hence (a,b) // A by A3, A4;

      end;

      assume (a,b) // A;

      then

      consider p, q such that

       A5: p <> q and

       A6: A = ( Line (p,q)) and

       A7: (a,b) // (p,q);

      (p,q) // (a,b) by A7, Th3;

      hence b in A by A2, A5, A6, Th21;

    end;

    theorem :: AFF_1:24

    a <> b & A = ( Line (a,b)) iff A is being_line & a in A & b in A & a <> b by Lm6, Th14;

    theorem :: AFF_1:25



     Th24: A is being_line & a in A & b in A & a <> b & LIN (a,b,x) implies x in A

    proof

      assume that

       A1: A is being_line and

       A2: a in A and

       A3: b in A and

       A4: a <> b and

       A5: LIN (a,b,x);

      A = ( Line (a,b)) by A1, A2, A3, A4, Lm6;

      hence thesis by A5, Def2;

    end;

    theorem :: AFF_1:26

    (ex a, b st (a,b) // A) implies A is being_line;

    theorem :: AFF_1:27



     Th26: c in A & d in A & A is being_line & c <> d implies ((a,b) // A iff (a,b) // (c,d))

    proof

      assume that

       A1: c in A and

       A2: d in A and

       A3: A is being_line and

       A4: c <> d;

      thus (a,b) // A implies (a,b) // (c,d)

      proof

        assume (a,b) // A;

        then

        consider p, q such that

         A5: p <> q and

         A6: A = ( Line (p,q)) and

         A7: (a,b) // (p,q);

        (p,q) // (c,d) by A1, A2, A5, A6, Th21;

        hence thesis by A5, A7, Th4;

      end;

      assume

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

      A = ( Line (c,d)) by A1, A2, A3, A4, Lm6;

      hence thesis by A4, A8;

    end;

    theorem :: AFF_1:28



     Th27: (a,b) // A implies ex c, d st c <> d & c in A & d in A & (a,b) // (c,d)

    proof

      assume (a,b) // A;

      then

      consider c, d such that

       A1: c <> d and

       A2: A = ( Line (c,d)) and

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



       A4: d in A by A2, Th14;

      c in A by A2, Th14;

      hence thesis by A1, A3, A4;

    end;

    theorem :: AFF_1:29



     Th28: a <> b implies (a,b) // ( Line (a,b)) by Th1;

    theorem :: AFF_1:30



     Th29: for A be being_line Subset of AS holds ((a,b) // A iff ex c, d st c <> d & c in A & d in A & (a,b) // (c,d))

    proof



       A1: (a,b) // A implies ex c, d st c <> d & c in A & d in A & (a,b) // (c,d) by Th27;

      let A be being_line Subset of AS;

      (ex c, d st c <> d & c in A & d in A & (a,b) // (c,d)) implies (a,b) // A

      proof

        assume ex c, d st c <> d & c in A & d in A & (a,b) // (c,d);

        then

        consider c, d such that

         A2: c <> d and

         A3: c in A and

         A4: d in A and

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

        A = ( Line (c,d)) by A2, A3, A4, Lm6;

        hence thesis by A2, A5;

      end;

      hence thesis by A1;

    end;

    theorem :: AFF_1:31

    for A be being_line Subset of AS st (a,b) // A & (c,d) // A holds (a,b) // (c,d)

    proof

      let A be being_line Subset of AS;

      assume that

       A1: (a,b) // A and

       A2: (c,d) // A;

      consider p, q such that

       A3: p <> q and

       A4: A = ( Line (p,q)) and

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



       A6: q in A by A4, Th14;

      p in A by A4, Th14;

      then (c,d) // (p,q) by A2, A3, A6, Th26;

      hence thesis by A3, A5, Th4;

    end;

    theorem :: AFF_1:32



     Th31: (a,b) // A & (a,b) // (p,q) & a <> b implies (p,q) // A

    proof

      assume that

       A1: (a,b) // A and

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

       A3: a <> b;



       A4: A is being_line by A1;

      then

      consider c, d such that

       A5: c <> d and

       A6: c in A and

       A7: d in A and

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

      (p,q) // (c,d) by A2, A3, A8, Th4;

      hence thesis by A4, A5, A6, A7, Th29;

    end;

    theorem :: AFF_1:33



     Th32: for A be being_line Subset of AS holds (a,a) // A

    proof

      let A be being_line Subset of AS;

      consider p, q such that

       A1: p <> q and

       A2: A = ( Line (p,q)) by Def3;

      (a,a) // (p,q) by Th2;

      hence thesis by A1, A2;

    end;

    theorem :: AFF_1:34



     Th33: (a,b) // A implies (b,a) // A

    proof

      assume

       A1: (a,b) // A;

      a <> b implies thesis by A1, Th1, Th31;

      hence thesis by A1;

    end;

    theorem :: AFF_1:35

    (a,b) // A & not a in A implies not b in A

    proof

      assume that

       A1: (a,b) // A and

       A2: not a in A and

       A3: b in A;



       A4: (b,a) // A by A1, Th33;

      A is being_line by A1;

      hence contradiction by A2, A3, A4, Th22;

    end;

    theorem :: AFF_1:36



     Th35: A // C implies A is being_line & C is being_line

    proof

      assume A // C;

      then ex a, b st A = ( Line (a,b)) & a <> b & (a,b) // C;

      hence thesis;

    end;

    theorem :: AFF_1:37



     Th36: A // C iff ex a, b, c, d st a <> b & c <> d & (a,b) // (c,d) & A = ( Line (a,b)) & C = ( Line (c,d))

    proof

      thus A // C implies ex a, b, c, d st a <> b & c <> d & (a,b) // (c,d) & A = ( Line (a,b)) & C = ( Line (c,d))

      proof

        assume A // C;

        then

        consider a, b such that

         A1: A = ( Line (a,b)) and

         A2: a <> b and

         A3: (a,b) // C;

        ex c, d st c <> d & C = ( Line (c,d)) & (a,b) // (c,d) by A3;

        hence thesis by A1, A2;

      end;

      given a, b, c, d such that

       A4: a <> b and

       A5: c <> d and

       A6: (a,b) // (c,d) and

       A7: A = ( Line (a,b)) and

       A8: C = ( Line (c,d));

      (a,b) // C by A5, A6, A8;

      hence thesis by A4, A7;

    end;

    theorem :: AFF_1:38



     Th37: for A,C be being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds (A // C iff (a,b) // (c,d))

    proof

      let A,C be being_line Subset of AS;

      assume that

       A1: a in A and

       A2: b in A and

       A3: c in C and

       A4: d in C and

       A5: a <> b and

       A6: c <> d;

      thus A // C implies (a,b) // (c,d)

      proof

        assume A // C;

        then

        consider p, q, r, s such that

         A7: p <> q and

         A8: r <> s and

         A9: (p,q) // (r,s) and

         A10: A = ( Line (p,q)) and

         A11: C = ( Line (r,s)) by Th36;

        (p,q) // (a,b) by A1, A2, A7, A10, Th21;

        then

         A12: (a,b) // (r,s) by A7, A9, Th4;

        (r,s) // (c,d) by A3, A4, A8, A11, Th21;

        hence thesis by A8, A12, Th4;

      end;



       A13: C = ( Line (c,d)) by A3, A4, A6, Lm6;

      assume

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

      A = ( Line (a,b)) by A1, A2, A5, Lm6;

      hence thesis by A5, A6, A14, A13, Th36;

    end;

    theorem :: AFF_1:39



     Th38: a in A & b in A & c in C & d in C & A // C implies (a,b) // (c,d)

    proof

      assume that

       A1: a in A and

       A2: b in A and

       A3: c in C and

       A4: d in C and

       A5: A // C;

      now



         A6: C is being_line by A5, Th35;

        assume that

         A7: a <> b and

         A8: c <> d;

        A is being_line by A5;

        hence thesis by A1, A2, A3, A4, A5, A7, A8, A6, Th37;

      end;

      hence thesis by Th2;

    end;

    theorem :: AFF_1:40

    a in A & b in A & A // C implies (a,b) // C

    proof

      assume that

       A1: a in A and

       A2: b in A and

       A3: A // C;



       A4: C is being_line by A3, Th35;

      now

        consider p, q such that

         A5: p in C and

         A6: q in C and

         A7: p <> q by A4, Th18;



         A8: C = ( Line (p,q)) by A4, A5, A6, A7, Lm6;

        (a,b) // (p,q) by A1, A2, A3, A5, A6, Th38;

        hence thesis by A7, A8;

      end;

      hence thesis;

    end;

    theorem :: AFF_1:41



     Th40: for A be being_line Subset of AS holds A // A

    proof

      let A be being_line Subset of AS;

      consider a, b such that

       A1: a <> b and

       A2: A = ( Line (a,b)) by Def3;

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

      hence thesis by A1, A2, Th36;

    end;

    definition

      let AS;

      let A,B be being_line Subset of AS;

      :: original: //

      redefine

      pred A // B;

      reflexivity by Th40;

    end

    theorem :: AFF_1:42



     Th41: A // C implies C // A

    proof

      assume A // C;

      then

      consider a, b, c, d such that

       A1: a <> b and

       A2: c <> d and

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

       A4: A = ( Line (a,b)) and

       A5: C = ( Line (c,d)) by Th36;

      (c,d) // (a,b) by A3, Th3;

      hence thesis by A1, A2, A4, A5, Th36;

    end;

    definition

      let AS, A, C;

      :: original: //

      redefine

      pred A // C;

      symmetry by Th41;

    end

    theorem :: AFF_1:43



     Th42: (a,b) // A & A // C implies (a,b) // C

    proof

      assume that

       A1: (a,b) // A and

       A2: A // C;

      consider p, q, c, d such that

       A3: p <> q and

       A4: c <> d and

       A5: (p,q) // (c,d) and

       A6: A = ( Line (p,q)) and

       A7: C = ( Line (c,d)) by A2, Th36;



       A8: q in A by A6, Th14;



       A9: A is being_line by A2;

      p in A by A6, Th14;

      then (a,b) // (p,q) by A1, A3, A8, A9, Th26;

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

      hence thesis by A4, A7;

    end;



     Lm7: A // C & C // D implies A // D

    proof

      assume that

       A1: A // C and

       A2: C // D;

      consider a, b, c, d such that

       A3: a <> b and

       A4: c <> d and

       A5: (a,b) // (c,d) and

       A6: A = ( Line (a,b)) and

       A7: C = ( Line (c,d)) by A1, Th36;



       A8: C is being_line by A2;



       A9: d in C by A7, Th14;



       A10: D is being_line by A2, Th35;

      then

      consider p, q such that

       A11: p <> q and

       A12: D = ( Line (p,q));



       A13: p in D by A12, Th14;



       A14: q in D by A12, Th14;

      c in C by A7, Th14;

      then (c,d) // (p,q) by A2, A4, A8, A10, A11, A13, A14, A9, Th37;

      then (a,b) // (p,q) by A4, A5, Th4;

      hence thesis by A3, A6, A11, A12, Th36;

    end;

    theorem :: AFF_1:44

    (A // C & C // D or A // C & D // C or C // A & C // D or C // A & D // C) implies A // D by Lm7;

    theorem :: AFF_1:45



     Th44: A // C & p in A & p in C implies A = C

    proof

      assume that

       A1: A // C and

       A2: p in A and

       A3: p in C;



       A4: for A, C, p holds A // C & p in A & p in C implies A c= C

      proof

        let A, C, p;

        assume that

         A5: A // C and

         A6: p in A and

         A7: p in C;



         A8: C is being_line by A5, Th35;



         A9: A is being_line by A5;

        let x be object;

        assume

         A10: x in A;

        then

        reconsider x9 = x as Element of AS;

        now

          consider q such that

           A11: p <> q and

           A12: q in C by A8, Th19;

          assume

           A13: x9 <> p;

          then A = ( Line (p,x9)) by A6, A9, A10, Lm6;

          then (p,x9) // C by A5, A13, Th28, Th42;

          then (p,x9) // (p,q) by A7, A8, A11, A12, Th26;

          then (p,q) // (p,x9) by Th3;

          then

           A14: LIN (p,q,x9);

          C = ( Line (p,q)) by A7, A8, A11, A12, Lm6;

          hence x in C by A14, Def2;

        end;

        hence x in C by A7;

      end;

      then

       A15: C c= A by A1, A2, A3;

      A c= C by A1, A2, A3, A4;

      hence thesis by A15, XBOOLE_0:def 10;

    end;

    theorem :: AFF_1:46

    x in K & not a in K & (a,b) // K implies (a = b or not LIN (x,a,b))

    proof

      assume that

       A1: x in K and

       A2: not a in K and

       A3: (a,b) // K;

      set A = ( Line (a,b));

      assume that

       A4: a <> b and

       A5: LIN (x,a,b);

       LIN (a,b,x) by A5, Th5;

      then

       A6: x in A by Def2;



       A7: a in A by Th14;

      A // K by A3, A4;

      hence contradiction by A1, A2, A6, A7, Th44;

    end;

    theorem :: AFF_1:47

    (a9,b9) // K & LIN (p,a,a9) & LIN (p,b,b9) & p in K & not a in K & a = b implies a9 = b9

    proof

      assume that

       A1: (a9,b9) // K and

       A2: LIN (p,a,a9) and

       A3: LIN (p,b,b9) and

       A4: p in K and

       A5: not a in K and

       A6: a = b;

      set A = ( Line (p,a));



       A7: b9 in A by A3, A6, Def2;



       A8: p in A by Th14;



       A9: a9 in A by A2, Def2;

      assume

       A10: a9 <> b9;

      A is being_line by A4, A5;

      then A = ( Line (a9,b9)) by A9, A7, A10, Lm6;

      then A // K by A1, A10;

      then A = K by A4, A8, Th44;

      hence contradiction by A5, Th14;

    end;

    theorem :: AFF_1:48

    for A be being_line Subset of AS st a in A & b in A & c in A & a <> b & (a,b) // (c,d) holds d in A

    proof

      let A be being_line Subset of AS;

      assume that

       A1: a in A and

       A2: b in A and

       A3: c in A and

       A4: a <> b and

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

      now

        set C = ( Line (c,d));



         A6: c in C by Th14;



         A7: d in C by Th14;

        assume

         A8: c <> d;

        then C is being_line;

        then A // C by A1, A2, A4, A5, A8, A6, A7, Th37;

        hence thesis by A3, A6, A7, Th44;

      end;

      hence thesis by A3;

    end;

    theorem :: AFF_1:49

    for A be being_line Subset of AS holds ex C st a in C & A // C

    proof

      let A be being_line Subset of AS;

      consider p, q such that

       A1: p <> q and

       A2: A = ( Line (p,q)) by Def3;

      consider b such that

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

       A4: a <> b by DIRAF: 40;

      set C = ( Line (a,b));



       A5: a in C by Th14;

      A // C by A1, A2, A3, A4, Th36;

      hence thesis by A5;

    end;

    theorem :: AFF_1:50

    A // C & A // D & p in C & p in D implies C = D by Lm7, Th44;

    theorem :: AFF_1:51

    A is being_line & a in A & b in A & c in A & d in A implies (a,b) // (c,d) by Th38, Th40;

    theorem :: AFF_1:52

    A is being_line & a in A & b in A implies (a,b) // A by Th22;

    theorem :: AFF_1:53

    (a,b) // A & (a,b) // C & a <> b implies A // C

    proof

      assume that

       A1: (a,b) // A and

       A2: (a,b) // C and

       A3: a <> b;



       A4: C is being_line by A2;

      then

      consider p, q such that

       A5: p <> q and

       A6: p in C and

       A7: q in C and

       A8: (a,b) // (p,q) by A2, Th29;



       A9: A is being_line by A1;

      then

      consider c, d such that

       A10: c <> d and

       A11: c in A and

       A12: d in A and

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

      (c,d) // (p,q) by A3, A13, A8, Th4;

      hence thesis by A9, A4, A10, A11, A12, A5, A6, A7, Th37;

    end;

    theorem :: AFF_1:54



     Th53: not LIN (o,a,b) & LIN (o,a,a9) & LIN (o,b,b9) & a9 = b9 implies a9 = o & b9 = o

    proof

      assume that

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

       A2: LIN (o,a,a9) and

       A3: LIN (o,b,b9) and

       A4: a9 = b9;

      set A = ( Line (o,a)), C = ( Line (o,b));



       A5: o in A by Th14;



       A6: o <> b by A1, Th6;

      then

       A7: C is being_line;



       A8: o <> a by A1, Th6;

      then

       A9: A is being_line;



       A10: a in A by Th14;

      then

       A11: a9 in A by A2, A8, A9, A5, Th24;



       A12: b in C by Th14;



       A13: o in C by Th14;

      then

       A14: b9 in C by A3, A6, A7, A12, Th24;

      A <> C by A1, A9, A5, A10, A12, Th20;

      hence thesis by A4, A9, A7, A5, A13, A14, A11, Th17;

    end;

    theorem :: AFF_1:55



     Th54: not LIN (o,a,b) & LIN (o,b,b9) & (a,b) // (a9,b9) & a9 = o implies b9 = o

    proof

      assume that

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

       A2: LIN (o,b,b9) and

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

       A4: a9 = o;

       A5:

      now

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

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

        then LIN (b,a,a9);

        hence contradiction by A1, A4, Th5;

      end;

      (a9,b) // (a9,b9) by A2, A4;

      hence thesis by A3, A4, A5, Th4;

    end;

    theorem :: AFF_1:56

     not LIN (o,a,b) & LIN (o,a,a9) & LIN (o,b,b9) & LIN (o,b,x) & (a,b) // (a9,b9) & (a,b) // (a9,x) implies b9 = x

    proof

      assume that

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

       A2: LIN (o,a,a9) and

       A3: LIN (o,b,b9) and

       A4: LIN (o,b,x) and

       A5: (a,b) // (a9,b9) and

       A6: (a,b) // (a9,x);

      set A = ( Line (o,a)), C = ( Line (o,b)), P = ( Line (a9,b9));



       A7: a9 in P by Th14;

      assume

       A8: b9 <> x;



       A9: a9 <> b9

      proof

        assume

         A10: a9 = b9;

        then a9 = o by A1, A2, A3, Th53;

        hence contradiction by A1, A4, A6, A8, A10, Th54;

      end;

      then

       A11: P is being_line;



       A12: o <> b by A1, Th6;

      then

       A13: C is being_line;



       A14: b9 in P by Th14;

      a <> b by A1, Th6;

      then (a9,b9) // (a9,x) by A5, A6, Th4;

      then LIN (a9,b9,x);

      then

       A15: x in P by A9, A11, A7, A14, Th24;



       A16: b in C by Th14;



       A17: o in C by Th14;

      then

       A18: x in C by A4, A12, A13, A16, Th24;

      b9 in C by A3, A12, A13, A17, A16, Th24;

      then

       A19: a9 in C by A8, A13, A11, A7, A14, A18, A15, Th17;



       A20: o <> a by A1, Th6;

      then

       A21: A is being_line;



       A22: a9 <> o

      proof

        assume

         A23: a9 = o;

        then b9 = o by A1, A3, A5, Th54;

        hence contradiction by A1, A4, A6, A8, A23, Th54;

      end;



       A24: o in A by Th14;



       A25: a in A by Th14;

      then a9 in A by A2, A20, A21, A24, Th24;

      then b in A by A22, A21, A13, A24, A17, A16, A19, Th17;

      hence contradiction by A1, A21, A24, A25, Th20;

    end;

    theorem :: AFF_1:57

    for a, b, A holds A is being_line & a in A & b in A & a <> b implies A = ( Line (a,b)) by Lm6;

    reserve AP for AffinPlane;

    reserve a,b,c,d,x,p,q for Element of AP;

    reserve A,C for Subset of AP;

    theorem :: AFF_1:58



     Th57: A is being_line & C is being_line & not A // C implies ex x st x in A & x in C

    proof

      assume that

       A1: A is being_line and

       A2: C is being_line and

       A3: not A // C;

      consider a, b such that

       A4: a <> b and

       A5: A = ( Line (a,b)) by A1;

      consider c, d such that

       A6: c <> d and

       A7: C = ( Line (c,d)) by A2;

       not (a,b) // (c,d) by A3, A4, A5, A6, A7, Th36;

      then

      consider x such that

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

       A9: (c,d) // (c,x) by DIRAF: 46;

       LIN (c,d,x) by A9;

      then

       A10: x in C by A7, Def2;

       LIN (a,b,x) by A8;

      then x in A by A5, Def2;

      hence thesis by A10;

    end;

    theorem :: AFF_1:59

    A is being_line & not (a,b) // A implies ex x st x in A & LIN (a,b,x)

    proof

      assume that

       A1: A is being_line and

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

      set C = ( Line (a,b));



       A3: not C // A

      proof



         A4: b in C by Th14;

        assume C // A;

        then

        consider p, q such that

         A5: C = ( Line (p,q)) and

         A6: p <> q and

         A7: (p,q) // A;

        a in C by Th14;

        then (p,q) // (a,b) by A5, A6, A4, Th21;

        hence contradiction by A2, A6, A7, Th31;

      end;

      a <> b by A1, A2, Th32;

      then C is being_line;

      then

      consider x such that

       A8: x in C and

       A9: x in A by A1, A3, Th57;

       LIN (a,b,x) by A8, Def2;

      hence thesis by A9;

    end;

    theorem :: AFF_1:60

     not (a,b) // (c,d) implies ex p st LIN (a,b,p) & LIN (c,d,p)

    proof

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

      then

      consider p such that

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

       A2: (c,d) // (c,p) by DIRAF: 46;



       A3: LIN (c,d,p) by A2;

       LIN (a,b,p) by A1;

      hence thesis by A3;

    end;