combgras.miz



    begin

    reserve k,n for Nat,

x,y,X,Y,Z for set;

    theorem :: COMBGRAS:1

    

     Th1: for a,b be set st a <> b & ( card a) = n & ( card b) = n holds ( card (a /\ b)) in n & (n + 1) c= ( card (a \/ b))

    proof

      let a,b be set;

      assume that

       A1: a <> b and

       A2: ( card a) = n and

       A3: ( card b) = n and

       A4: not ( card (a /\ b)) in n or not (n + 1) c= ( card (a \/ b));

      n c= ( card (a /\ b)) or ( card (a \/ b)) in ( Segm (n + 1)) by A4, ORDINAL1: 16;

      then n c= ( card (a /\ b)) or ( card (a \/ b)) in ( succ ( Segm n)) by NAT_1: 38;

      then

       A5: n c= ( card (a /\ b)) or ( card (a \/ b)) c= n by ORDINAL1: 22;

      n c= ( card (a \/ b)) & ( card (a /\ b)) c= n by A2, CARD_1: 11, XBOOLE_1: 7, XBOOLE_1: 17;

      then

       A6: ( card a) = ( card (a /\ b)) & ( card (a /\ b)) = ( card b) or ( card (a \/ b)) = ( card a) & ( card (a \/ b)) = ( card b) by A2, A3, A5, XBOOLE_0:def 10;

      

       A7: a c= (a \/ b) & b c= (a \/ b) by XBOOLE_1: 7;

      a is finite set & b is finite set by A2, A3;

      then a = (a /\ b) & b = (a /\ b) or a = (a \/ b) & b = (a \/ b) by A7, A6, CARD_2: 102, XBOOLE_1: 17;

      hence contradiction by A1;

    end;

    theorem :: COMBGRAS:2

    

     Th2: for a,b be set st ( card a) = (n + k) & ( card b) = (n + k) holds ( card (a /\ b)) = n iff ( card (a \/ b)) = (n + (2 * k))

    proof

      let a,b be set;

      assume that

       A1: ( card a) = (n + k) and

       A2: ( card b) = (n + k);

      

       A3: a is finite by A1;

      

       A4: b is finite by A2;

      thus ( card (a /\ b)) = n implies ( card (a \/ b)) = (n + (2 * k))

      proof

        assume ( card (a /\ b)) = n;

        then ( card (a \/ b)) = (((n + k) + (n + k)) - n) by A1, A2, A3, A4, CARD_2: 45;

        hence thesis;

      end;

      thus ( card (a \/ b)) = (n + (2 * k)) implies ( card (a /\ b)) = n

      proof

        reconsider m = ( card (a /\ b)) as Nat by A3;

        assume ( card (a \/ b)) = (n + (2 * k));

        then (n + (2 * k)) = (((n + k) + (n + k)) - m) by A1, A2, A3, A4, CARD_2: 45;

        hence thesis;

      end;

    end;

    theorem :: COMBGRAS:3

    

     Th3: ( card X) c= ( card Y) iff ex f be Function st f is one-to-one & X c= ( dom f) & (f .: X) c= Y

    proof

      thus ( card X) c= ( card Y) implies ex f be Function st f is one-to-one & X c= ( dom f) & (f .: X) c= Y

      proof

        assume ( card X) c= ( card Y);

        then

        consider f be Function such that

         A1: f is one-to-one & ( dom f) = X & ( rng f) c= Y by CARD_1: 10;

        take f;

        thus thesis by A1, RELAT_1: 113;

      end;

      given f be Function such that

       A2: f is one-to-one and

       A3: X c= ( dom f) and

       A4: (f .: X) c= Y;

      

       A5: ( rng (f | X)) c= Y

      proof

        let y be object;

        assume y in ( rng (f | X));

        then

        consider x be object such that

         A6: x in ( dom (f | X)) & y = ((f | X) . x) by FUNCT_1:def 3;

        x in X & y = (f . x) by A3, A6, FUNCT_1: 47, RELAT_1: 62;

        then y in (f .: X) by A3, FUNCT_1:def 6;

        hence thesis by A4;

      end;

      (f | X) is one-to-one & ( dom (f | X)) = X by A2, A3, FUNCT_1: 52, RELAT_1: 62;

      hence thesis by A5, CARD_1: 10;

    end;

    theorem :: COMBGRAS:4

    

     Th4: for f be Function st f is one-to-one & X c= ( dom f) holds ( card (f .: X)) = ( card X)

    proof

      let f be Function;

      assume f is one-to-one & X c= ( dom f);

      then ( card (f .: X)) c= ( card X) & ( card X) c= ( card (f .: X)) by Th3, CARD_1: 67;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: COMBGRAS:5

    

     Th5: (X \ Y) = (X \ Z) & Y c= X & Z c= X implies Y = Z

    proof

      assume that

       A1: (X \ Y) = (X \ Z) and

       A2: Y c= X and

       A3: Z c= X;

      

       A4: (Y \ Z) c= X by A2;

      (X \ Z) misses Y by A1, XBOOLE_1: 106;

      then (Y \ Z) = {} by A4, XBOOLE_1: 67, XBOOLE_1: 81;

      then

       A5: Y c= Z by XBOOLE_1: 37;

      

       A6: (Z \ Y) c= X by A3;

      (X \ Y) misses Z by A1, XBOOLE_1: 106;

      then (Z \ Y) = {} by A6, XBOOLE_1: 67, XBOOLE_1: 81;

      then Z c= Y by XBOOLE_1: 37;

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    theorem :: COMBGRAS:6

    

     Th6: for Y be non empty set holds for p be Function of X, Y st p is one-to-one holds for x1,x2 be Subset of X holds x1 <> x2 implies (p .: x1) <> (p .: x2)

    proof

      let Y be non empty set;

      let p be Function of X, Y such that

       A1: p is one-to-one;

      let x1 be Subset of X;

      let x2 be Subset of X;

      

       A2: X = ( dom p) by FUNCT_2:def 1;

      

       A3: not x1 c= x2 implies (p .: x1) <> (p .: x2)

      proof

        assume not x1 c= x2;

        then

        consider a be object such that

         A4: a in x1 and

         A5: not a in x2;

         not (p . a) in (p .: x2)

        proof

          assume (p . a) in (p .: x2);

          then ex b be object st b in ( dom p) & b in x2 & (p . a) = (p . b) by FUNCT_1:def 6;

          hence contradiction by A1, A2, A4, A5;

        end;

        hence thesis by A2, A4, FUNCT_1:def 6;

      end;

      

       A6: not x2 c= x1 implies (p .: x1) <> (p .: x2)

      proof

        assume not x2 c= x1;

        then

        consider a be object such that

         A7: a in x2 and

         A8: not a in x1;

         not (p . a) in (p .: x1)

        proof

          assume (p . a) in (p .: x1);

          then ex b be object st b in ( dom p) & b in x1 & (p . a) = (p . b) by FUNCT_1:def 6;

          hence contradiction by A1, A2, A7, A8;

        end;

        hence thesis by A2, A7, FUNCT_1:def 6;

      end;

      assume x1 <> x2;

      hence thesis by A3, A6, XBOOLE_0:def 10;

    end;

    theorem :: COMBGRAS:7

    

     Th7: for a,b,c be set st ( card a) = (n - 1) & ( card b) = (n - 1) & ( card c) = (n - 1) & ( card (a /\ b)) = (n - 2) & ( card (a /\ c)) = (n - 2) & ( card (b /\ c)) = (n - 2) & 2 <= n holds (3 <= n implies ( card ((a /\ b) /\ c)) = (n - 2) & ( card ((a \/ b) \/ c)) = (n + 1) or ( card ((a /\ b) /\ c)) = (n - 3) & ( card ((a \/ b) \/ c)) = n) & (n = 2 implies ( card ((a /\ b) /\ c)) = (n - 2) & ( card ((a \/ b) \/ c)) = (n + 1))

    proof

      let a,b,c be set;

      assume that

       A1: ( card a) = (n - 1) and

       A2: ( card b) = (n - 1) and

       A3: ( card c) = (n - 1) and

       A4: ( card (a /\ b)) = (n - 2) and

       A5: ( card (a /\ c)) = (n - 2) and

       A6: ( card (b /\ c)) = (n - 2) and

       A7: 2 <= n;

      2 <= (n + 1) by A7, NAT_1: 13;

      then

       A8: (2 - 1) <= ((n + 1) - 1) by XREAL_1: 13;

      then a is finite by A1, NAT_1: 21;

      then

      reconsider a as finite set;

      

       A9: ( card (a \ (a /\ b))) = ((n - 1) - (n - 2)) by A1, A4, CARD_2: 44, XBOOLE_1: 17;

      then

      consider x1 be object such that

       A10: {x1} = (a \ (a /\ b)) by CARD_2: 42;

      b is finite by A2, A8, NAT_1: 21;

      then

      reconsider b as finite set;

      ( card (b \ (a /\ b))) = ((n - 1) - (n - 2)) by A2, A4, CARD_2: 44, XBOOLE_1: 17;

      then

      consider x2 be object such that

       A11: {x2} = (b \ (a /\ b)) by CARD_2: 42;

      c is finite by A3, A8, NAT_1: 21;

      then ( card (c \ (a /\ c))) = ((n - 1) - (n - 2)) by A3, A5, CARD_2: 44, XBOOLE_1: 17;

      then

      consider x3 be object such that

       A12: {x3} = (c \ (a /\ c)) by CARD_2: 42;

      

       A13: a = ((a /\ b) \/ {x1}) by A10, XBOOLE_1: 17, XBOOLE_1: 45;

      

       A14: ((a /\ b) /\ c) = ((b /\ c) /\ a) by XBOOLE_1: 16;

      

       A15: (a /\ c) c= a by XBOOLE_1: 17;

      

       A16: ((a /\ b) /\ c) = ((a /\ c) /\ b) by XBOOLE_1: 16;

      

       A17: b = ((a /\ b) \/ {x2}) by A11, XBOOLE_1: 17, XBOOLE_1: 45;

      x3 in {x3} by TARSKI:def 1;

      then

       A18: not x3 in (a /\ c) by A12, XBOOLE_0:def 5;

      

       A19: c = ((a /\ c) \/ {x3}) by A12, XBOOLE_1: 17, XBOOLE_1: 45;

      

       A20: x2 in {x2} by TARSKI:def 1;

      then

       A21: not x2 in (a /\ b) by A11, XBOOLE_0:def 5;

      

       A22: x1 in {x1} by TARSKI:def 1;

      then

       A23: not x1 in (a /\ b) by A10, XBOOLE_0:def 5;

      then

       A24: x1 <> x2 by A10, A11, A20, XBOOLE_0:def 4;

      

       A25: (a /\ b) c= b by XBOOLE_1: 17;

      

       A26: 3 <= n implies ( card ((a /\ b) /\ c)) = (n - 2) & ( card ((a \/ b) \/ c)) = (n + 1) or ( card ((a /\ b) /\ c)) = (n - 3) & ( card ((a \/ b) \/ c)) = n

      proof

        assume 3 <= n;

        

         A27: x1 in c implies ( card ((a /\ b) /\ c)) = (n - 3) & ( card ((a \/ b) \/ c)) = n

        proof

          ((a /\ b) /\ c) misses {x1}

          proof

            assume ((a /\ b) /\ c) meets {x1};

            then not (((a /\ b) /\ c) /\ {x1}) = {} by XBOOLE_0:def 7;

            then

            consider x be object such that

             A28: x in (((a /\ b) /\ c) /\ {x1}) by XBOOLE_0:def 1;

            x in {x1} by A28, XBOOLE_0:def 4;

            then

             A29: x = x1 by TARSKI:def 1;

            x in ((a /\ b) /\ c) by A28, XBOOLE_0:def 4;

            hence contradiction by A23, A29, XBOOLE_0:def 4;

          end;

          then

           A30: ((a /\ b) /\ c) c= ((a /\ c) \ {x1}) by A16, XBOOLE_1: 17, XBOOLE_1: 86;

          ((a /\ c) \ {x1}) c= b

          proof

            let z be object;

            assume

             A31: z in ((a /\ c) \ {x1});

            then not z in {x1} by XBOOLE_0:def 5;

            then z in a & not z in (a \ (a /\ b)) & not z in a or z in (a /\ b) by A10, A31, XBOOLE_0:def 4, XBOOLE_0:def 5;

            hence thesis by XBOOLE_0:def 4;

          end;

          then ((a /\ c) \ {x1}) c= ((a /\ c) /\ b) by XBOOLE_1: 19;

          then

           A32: ((a /\ c) \ {x1}) c= ((a /\ b) /\ c) by XBOOLE_1: 16;

          

           A33: (a /\ b) misses {x1, x2}

          proof

            assume (a /\ b) meets {x1, x2};

            then ((a /\ b) /\ {x1, x2}) <> {} by XBOOLE_0:def 7;

            then

            consider z1 be object such that

             A34: z1 in ((a /\ b) /\ {x1, x2}) by XBOOLE_0:def 1;

            z1 in (a /\ b) & z1 in {x1, x2} by A34, XBOOLE_0:def 4;

            hence contradiction by A23, A21, TARSKI:def 2;

          end;

          assume x1 in c;

          then x1 in (a /\ c) by A10, A22, XBOOLE_0:def 4;

          then

           A35: {x1} c= (a /\ c) by ZFMISC_1: 31;

          (a \/ b) = ((a /\ b) \/ ( {x1} \/ {x2})) by A13, A17, XBOOLE_1: 5;

          then

           A36: (a \/ b) = ((a /\ b) \/ {x1, x2}) by ENUMSET1: 1;

          ( card {x1}) = 1 by CARD_1: 30;

          then

           A37: ( card ((a /\ c) \ {x1})) = ((n - 2) - 1) by A5, A35, CARD_2: 44;

          then

           A38: ( card ((a /\ b) /\ c)) = (n - 3) by A30, A32, XBOOLE_0:def 10;

          x3 = x2

          proof

            assume

             A39: x2 <> x3;

            (b /\ c) c= ((a /\ b) /\ c)

            proof

              let z1 be object;

              assume

               A40: z1 in (b /\ c);

              then z1 in b by XBOOLE_0:def 4;

              then z1 in (a /\ b) or z1 in {x2} by A17, XBOOLE_0:def 3;

              then

               A41: z1 in (a /\ b) or z1 = x2 by TARSKI:def 1;

              z1 in c by A40, XBOOLE_0:def 4;

              then z1 in (a /\ c) or z1 in {x3} by A19, XBOOLE_0:def 3;

              then (z1 in (a /\ b) or z1 in {x2}) & z1 in (a /\ c) or z1 in (a /\ b) & (z1 in (a /\ c) or z1 in {x3}) by A39, A41, TARSKI:def 1;

              hence thesis by A25, A11, A12, A16, XBOOLE_0:def 4;

            end;

            then ( Segm ( card (b /\ c))) c= ( Segm ( card ((a /\ b) /\ c))) by CARD_1: 11;

            then (( - 2) + n) <= (( - 3) + n) by A6, A38, NAT_1: 39;

            hence contradiction by XREAL_1: 6;

          end;

          then

           A42: c c= (a \/ b) by A15, A11, A19, XBOOLE_1: 13;

          ( card {x1, x2}) = 2 by A24, CARD_2: 57;

          then ( card (a \/ b)) = ((n - 2) + 2) by A4, A36, A33, CARD_2: 40;

          hence thesis by A37, A30, A32, A42, XBOOLE_0:def 10, XBOOLE_1: 12;

        end;

         not x1 in c implies ( card ((a /\ b) /\ c)) = (n - 2) & ( card ((a \/ b) \/ c)) = (n + 1)

        proof

          

           A43: x1 <> x3 by A10, A12, A22, A18, XBOOLE_0:def 4;

          

           A44: ( card (a \ {x1})) = ((n - 1) - 1) by A1, A9, A10, CARD_2: 44;

          assume

           A45: not x1 in c;

          

           A46: (a /\ c) misses {x1} & (a /\ b) misses {x1}

          proof

            assume not (a /\ c) misses {x1} or not (a /\ b) misses {x1};

            then ((a /\ c) /\ {x1}) <> {} or ((a /\ b) /\ {x1}) <> {} by XBOOLE_0:def 7;

            then

            consider z2 be object such that

             A47: z2 in ((a /\ c) /\ {x1}) or z2 in ((a /\ b) /\ {x1}) by XBOOLE_0:def 1;

            z2 in (a /\ c) & z2 in {x1} or z2 in (a /\ b) & z2 in {x1} by A47, XBOOLE_0:def 4;

            then z2 in a & z2 in c & z2 = x1 or z2 in (a /\ b) & z2 = x1 by TARSKI:def 1, XBOOLE_0:def 4;

            hence contradiction by A10, A22, A45, XBOOLE_0:def 5;

          end;

          then (a /\ c) c= (a \ {x1}) by XBOOLE_1: 17, XBOOLE_1: 86;

          then

           A48: (a /\ c) = (a \ {x1}) by A5, A44, CARD_2: 102;

          (a /\ b) c= (a \ {x1}) by A46, XBOOLE_1: 17, XBOOLE_1: 86;

          then

           A49: (a /\ b) = (a \ {x1}) by A4, A44, CARD_2: 102;

          

           A50: (a /\ b) misses {x1, x2, x3}

          proof

            assume not (a /\ b) misses {x1, x2, x3};

            then ((a /\ b) /\ {x1, x2, x3}) <> {} by XBOOLE_0:def 7;

            then

            consider z3 be object such that

             A51: z3 in ((a /\ b) /\ {x1, x2, x3}) by XBOOLE_0:def 1;

            z3 in (a /\ b) & z3 in {x1, x2, x3} by A51, XBOOLE_0:def 4;

            hence contradiction by A23, A21, A18, A48, A49, ENUMSET1:def 1;

          end;

          (a \/ b) = ((a /\ b) \/ ( {x1} \/ {x2})) by A13, A17, XBOOLE_1: 5;

          then (a \/ b) = ((a /\ b) \/ {x1, x2}) by ENUMSET1: 1;

          then ((a \/ b) \/ c) = ((a /\ b) \/ ( {x1, x2} \/ {x3})) by A19, A48, A49, XBOOLE_1: 5;

          then

           A52: ((a \/ b) \/ c) = ((a /\ b) \/ {x1, x2, x3}) by ENUMSET1: 3;

          ((a /\ b) /\ (a /\ c)) = (a /\ b) by A48, A49;

          then (((b /\ a) /\ a) /\ c) = (a /\ b) by XBOOLE_1: 16;

          then

           A53: ((b /\ (a /\ a)) /\ c) = (a /\ b) by XBOOLE_1: 16;

          then ((a /\ b) /\ c) = (b /\ c) by A4, A6, A14, CARD_2: 102, XBOOLE_1: 17;

          then x2 <> x3 by A11, A12, A20, A21, A53, XBOOLE_0:def 4;

          then ( card {x1, x2, x3}) = 3 by A24, A43, CARD_2: 58;

          then ( card ((a \/ b) \/ c)) = ((n - 2) + 3) by A4, A52, A50, CARD_2: 40;

          hence thesis by A4, A53;

        end;

        hence thesis by A27;

      end;

      

       A54: x1 <> x3 by A10, A12, A22, A18, XBOOLE_0:def 4;

      n = 2 implies ( card ((a /\ b) /\ c)) = (n - 2) & ( card ((a \/ b) \/ c)) = (n + 1)

      proof

        assume

         A55: n = 2;

        then

         A56: (a /\ b) = {} by A4;

        then ((a /\ b) /\ c) = (a /\ c) by A4, A5;

        then ((a \/ b) \/ c) = (((a /\ b) /\ c) \/ ( {x1, x2} \/ {x3})) by A10, A11, A12, A56, ENUMSET1: 1;

        then

         A57: ((a \/ b) \/ c) = (((a /\ b) /\ c) \/ {x1, x2, x3}) by ENUMSET1: 3;

        ((a /\ b) /\ c) = (b /\ c) by A4, A6, A56;

        then x2 <> x3 by A11, A12, A20, A56, XBOOLE_0:def 4;

        hence thesis by A24, A54, A55, A56, A57, CARD_2: 58;

      end;

      hence thesis by A26;

    end;

    theorem :: COMBGRAS:8

    for P1,P2 be IncProjStr st the IncProjStr of P1 = the IncProjStr of P2 holds for A1 be POINT of P1, A2 be POINT of P2 st A1 = A2 holds for L1 be LINE of P1, L2 be LINE of P2 st L1 = L2 holds A1 on L1 implies A2 on L2;

    theorem :: COMBGRAS:9

    

     Th9: for P1,P2 be IncProjStr st the IncProjStr of P1 = the IncProjStr of P2 holds for A1 be Subset of the Points of P1 holds for A2 be Subset of the Points of P2 st A1 = A2 holds for L1 be LINE of P1, L2 be LINE of P2 st L1 = L2 holds A1 on L1 implies A2 on L2

    proof

      let P1,P2 be IncProjStr;

      assume

       A1: the IncProjStr of P1 = the IncProjStr of P2;

      let A1 be Subset of the Points of P1, A2 be Subset of the Points of P2;

      assume

       A2: A1 = A2;

      let L1 be LINE of P1, L2 be LINE of P2;

      assume that

       A3: L1 = L2 and

       A4: A1 on L1;

      thus A2 on L2

      proof

        let A be POINT of P2;

        consider B be POINT of P1 such that

         A5: A = B by A1;

        assume A in A2;

        then B on L1 by A2, A4, A5;

        then [A, L2] in the Inc of P2 by A1, A3, A5;

        hence thesis;

      end;

    end;

    registration

      cluster with_non-trivial_lines linear up-2-rank strict for IncProjStr;

      existence

      proof

        set P = the IncSpace-like strict IncStruct;

        take IT = IncProjStr (# the Points of P, the Lines of P, the Inc of P #);

        thus for L be LINE of IT holds ex A,B be POINT of IT st A <> B & {A, B} on L

        proof

          let L be LINE of IT;

          reconsider L9 = L as LINE of P;

          consider A9,B9 be POINT of P such that

           A1: A9 <> B9 & {A9, B9} on L9 by INCSP_1:def 8;

          reconsider A = A9, B = B9 as POINT of IT;

          take A, B;

          thus thesis by A1, Th9;

        end;

        thus IT is linear

        proof

          let A,B be POINT of IT;

          reconsider A9 = A, B9 = B as POINT of P;

          consider L9 be LINE of P such that

           A2: {A9, B9} on L9 by INCSP_1:def 9;

          reconsider L = L9 as LINE of IT;

          take L;

          A9 on L9 & B9 on L9 by A2, INCSP_1: 1;

          hence thesis;

        end;

        thus for A,B be POINT of IT, K,L be LINE of IT st A <> B & {A, B} on K & {A, B} on L holds K = L

        proof

          let A,B be POINT of IT, K,L be LINE of IT;

          assume that

           A3: A <> B and

           A4: {A, B} on K & {A, B} on L;

          reconsider K9 = K, L9 = L as LINE of P;

          reconsider A9 = A, B9 = B as POINT of P;

           {A9, B9} on K9 & {A9, B9} on L9 by A4, Th9;

          hence thesis by A3, INCSP_1:def 10;

        end;

        thus thesis;

      end;

    end

    begin

    definition

      mode PartialLinearSpace is with_non-trivial_lines up-2-rank IncProjStr;

    end

    definition

      let k be Nat;

      let X be non empty set;

      :: COMBGRAS:def1

      func G_ (k,X) -> strict PartialLinearSpace means

      : Def1: the Points of it = { A where A be Subset of X : ( card A) = k } & the Lines of it = { L where L be Subset of X : ( card L) = (k + 1) } & the Inc of it = (( RelIncl ( bool X)) /\ [:the Points of it , the Lines of it :]);

      existence

      proof

        set L = { B where B be Subset of X : ( card B) = (k + 1) };

        set P = { A where A be Subset of X : ( card A) = k };

        set I = (( RelIncl ( bool X)) /\ [:P, L:]);

        consider B be set such that

         A3: B c= X & ( card B) = (k + 1) by A2, CARD_FIL: 36;

        B in L by A3;

        then

        reconsider L as non empty set;

        k <= (k + 1) by NAT_1: 11;

        then ( Segm k) c= ( Segm (k + 1)) by NAT_1: 39;

        then k c= ( card X) by A2;

        then

        consider A be set such that

         A4: A c= X & ( card A) = k by CARD_FIL: 36;

        A in P by A4;

        then

        reconsider P as non empty set;

        reconsider I as Relation of P, L by XBOOLE_1: 17;

        set G = IncProjStr (# P, L, I #);

        

         A5: G is up-2-rank

        proof

          let a,b be POINT of G;

          let l1,l2 be LINE of G;

          assume that

           A6: a <> b and

           A7: {a, b} on l1 and

           A8: {a, b} on l2;

          b in P;

          then

           A9: ex B be Subset of X st b = B & ( card B) = k;

          a in P;

          then

           A10: ex A be Subset of X st a = A & ( card A) = k;

          then

           A11: (k + 1) c= ( card (a \/ b)) by A9, A6, Th1;

          l1 in L;

          then

           A12: ex C be Subset of X st l1 = C & ( card C) = (k + 1);

          then

           A13: l1 is finite;

          

           A14: b in {a, b} by TARSKI:def 2;

          then b on l1 by A7;

          then [b, l1] in I;

          then [b, l1] in ( RelIncl ( bool X)) by XBOOLE_0:def 4;

          then

           A15: b c= l1 by A9, A12, WELLORD2:def 1;

          l2 in L;

          then

           A16: ex D be Subset of X st l2 = D & ( card D) = (k + 1);

          then

           A17: l2 is finite;

          

           A18: a in {a, b} by TARSKI:def 2;

          then a on l2 by A8;

          then [a, l2] in I;

          then [a, l2] in ( RelIncl ( bool X)) by XBOOLE_0:def 4;

          then

           A19: a c= l2 by A10, A16, WELLORD2:def 1;

          b on l2 by A14, A8;

          then [b, l2] in I;

          then [b, l2] in ( RelIncl ( bool X)) by XBOOLE_0:def 4;

          then

           A20: b c= l2 by A9, A16, WELLORD2:def 1;

          then (a \/ b) c= l2 by A19, XBOOLE_1: 8;

          then ( card (a \/ b)) c= (k + 1) by A16, CARD_1: 11;

          then

           A21: ( card (a \/ b)) = (k + 1) by A11, XBOOLE_0:def 10;

          a on l1 by A18, A7;

          then [a, l1] in I;

          then [a, l1] in ( RelIncl ( bool X)) by XBOOLE_0:def 4;

          then a c= l1 by A10, A12, WELLORD2:def 1;

          then (a \/ b) = l1 by A12, A15, A21, A13, CARD_2: 102, XBOOLE_1: 8;

          hence thesis by A16, A19, A20, A21, A17, CARD_2: 102, XBOOLE_1: 8;

        end;

        G is with_non-trivial_lines

        proof

          let l be LINE of G;

          l in L;

          then

          consider C be Subset of X such that

           A22: l = C and

           A23: ( card C) = (k + 1);

          1 < (k + 1) by A1, XREAL_1: 29;

          then (1 + 1) <= (k + 1) by NAT_1: 13;

          then ( Segm 2) c= ( Segm (k + 1)) by NAT_1: 39;

          then

          consider a,b be object such that

           A24: a in C and

           A25: b in C and

           A26: a <> b by A23, PENCIL_1: 2;

          reconsider x = (C \ {a}), y = (C \ {b}) as Subset of X;

          ( card x) = k by A23, A24, STIRL2_1: 55;

          then

           A27: x in P;

          ( card y) = k by A23, A25, STIRL2_1: 55;

          then y in P;

          then

          reconsider x, y as POINT of G by A27;

          take x, y;

           not b in {a} by A26, TARSKI:def 1;

          then b in {b} & b in x by A25, TARSKI:def 1, XBOOLE_0:def 5;

          hence x <> y by XBOOLE_0:def 5;

          

           A28: C c= ( {a} \/ C) & C c= ( {b} \/ C) by XBOOLE_1: 7;

           {x, y} on l

          proof

            let z be POINT of G;

            assume z in {x, y};

            then

             A29: z = x or z = y by TARSKI:def 2;

            then z c= l by A22, A28, XBOOLE_1: 43;

            then [z, l] in ( RelIncl ( bool X)) by A22, A29, WELLORD2:def 1;

            then [z, l] in I by XBOOLE_0:def 4;

            hence thesis;

          end;

          hence thesis;

        end;

        hence thesis by A5;

      end;

      uniqueness ;

    end

    theorem :: COMBGRAS:10

    

     Th10: for k be Nat holds for X be non empty set st 0 < k & (k + 1) c= ( card X) holds for A be POINT of ( G_ (k,X)) holds for L be LINE of ( G_ (k,X)) holds A on L iff A c= L

    proof

      let k be Nat;

      let X be non empty set;

      assume

       A1: 0 < k & (k + 1) c= ( card X);

      then

       A2: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by Def1;

      let A be POINT of ( G_ (k,X));

      A in the Points of ( G_ (k,X));

      then

       A3: ex A1 be Subset of X st A1 = A & ( card A1) = k by A2;

      

       A4: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, Def1;

      let L be LINE of ( G_ (k,X));

      L in the Lines of ( G_ (k,X));

      then

       A5: ex L1 be Subset of X st L1 = L & ( card L1) = (k + 1) by A4;

      

       A6: the Inc of ( G_ (k,X)) = (( RelIncl ( bool X)) /\ [:the Points of ( G_ (k,X)), the Lines of ( G_ (k,X)):]) by A1, Def1;

      thus A on L implies A c= L

      proof

        assume A on L;

        then [A, L] in the Inc of ( G_ (k,X));

        then [A, L] in ( RelIncl ( bool X)) by A6, XBOOLE_0:def 4;

        hence thesis by A3, A5, WELLORD2:def 1;

      end;

      thus A c= L implies A on L

      proof

        assume A c= L;

        then [A, L] in ( RelIncl ( bool X)) by A3, A5, WELLORD2:def 1;

        then [A, L] in the Inc of ( G_ (k,X)) by A6, XBOOLE_0:def 4;

        hence thesis;

      end;

    end;

    theorem :: COMBGRAS:11

    

     Th11: for k be Element of NAT holds for X be non empty set st 0 < k & (k + 1) c= ( card X) holds ( G_ (k,X)) is Vebleian

    proof

      let k be Element of NAT ;

      let X be non empty set;

      k <= (k + 1) by NAT_1: 11;

      then

       A1: ( Segm k) c= ( Segm (k + 1)) by NAT_1: 39;

      assume

       A2: 0 < k & (k + 1) c= ( card X);

      then

       A3: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by Def1;

      let A1,A2,A3,A4,A5,A6 be POINT of ( G_ (k,X)), L1,L2,L3,L4 be LINE of ( G_ (k,X));

      assume that

       A4: A1 on L1 and

       A5: A2 on L1 and

       A6: A3 on L2 and

       A7: A4 on L2 and

       A8: A5 on L1 & A5 on L2 and

       A9: A1 on L3 and

       A10: A3 on L3 and

       A11: A2 on L4 and

       A12: A4 on L4 and

       A13: ( not A5 on L3) & not A5 on L4 and

       A14: L1 <> L2;

      

       A15: A2 c= L1 & A4 c= L2 by A2, A5, A7, Th10;

      

       A16: A1 <> A3 & A2 <> A4

      proof

        assume A1 = A3 or A2 = A4;

        then {A1, A5} on L1 & {A1, A5} on L2 or {A2, A5} on L1 & {A2, A5} on L2 by A4, A5, A6, A7, A8, INCSP_1: 1;

        hence contradiction by A9, A11, A13, A14, INCSP_1:def 10;

      end;

      

       A17: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A2, Def1;

      A5 c= L1 & A5 c= L2 by A2, A8, Th10;

      then

       A18: A5 c= (L1 /\ L2) by XBOOLE_1: 19;

      A5 in the Points of ( G_ (k,X));

      then ex B5 be Subset of X st B5 = A5 & ( card B5) = k by A3;

      then

       A19: k c= ( card (L1 /\ L2)) by A18, CARD_1: 11;

      L2 in the Lines of ( G_ (k,X));

      then

       A20: ex K2 be Subset of X st K2 = L2 & ( card K2) = (k + 1) by A17;

      A3 in the Points of ( G_ (k,X));

      then

       A21: ex B3 be Subset of X st B3 = A3 & ( card B3) = k by A3;

      A1 in the Points of ( G_ (k,X));

      then ex B1 be Subset of X st B1 = A1 & ( card B1) = k by A3;

      then

       A22: (k + 1) c= ( card (A1 \/ A3)) by A21, A16, Th1;

      

       A23: A1 c= L1 & A3 c= L2 by A2, A4, A6, Th10;

      L3 in the Lines of ( G_ (k,X));

      then

       A24: ex K3 be Subset of X st K3 = L3 & ( card K3) = (k + 1) by A17;

      then

       A25: L3 is finite;

      A4 in the Points of ( G_ (k,X));

      then

       A26: ex B4 be Subset of X st B4 = A4 & ( card B4) = k by A3;

      A2 in the Points of ( G_ (k,X));

      then ex B2 be Subset of X st B2 = A2 & ( card B2) = k by A3;

      then

       A27: (k + 1) c= ( card (A2 \/ A4)) by A26, A16, Th1;

      L4 in the Lines of ( G_ (k,X));

      then

       A28: ex K4 be Subset of X st K4 = L4 & ( card K4) = (k + 1) by A17;

      then

       A29: L4 is finite;

      

       A30: A2 c= L4 & A4 c= L4 by A2, A11, A12, Th10;

      then (A2 \/ A4) c= L4 by XBOOLE_1: 8;

      then ( card (A2 \/ A4)) c= (k + 1) by A28, CARD_1: 11;

      then ( card (A2 \/ A4)) = (k + 1) by A27, XBOOLE_0:def 10;

      then (A2 \/ A4) = L4 by A28, A30, A29, CARD_2: 102, XBOOLE_1: 8;

      then

       A31: L4 c= (L1 \/ L2) by A15, XBOOLE_1: 13;

      L1 in the Lines of ( G_ (k,X));

      then

       A32: ex K1 be Subset of X st K1 = L1 & ( card K1) = (k + 1) by A17;

      then ( card (L1 /\ L2)) in ( Segm (k + 1)) by A20, A14, Th1;

      then ( card (L1 /\ L2)) in ( succ ( Segm k)) by NAT_1: 38;

      then ( card (L1 /\ L2)) c= k by ORDINAL1: 22;

      then ( card (L1 /\ L2)) = k by A19, XBOOLE_0:def 10;

      then

       A33: ( card (L1 \/ L2)) = (k + (2 * 1)) by A32, A20, Th2;

      

       A34: A1 c= L3 & A3 c= L3 by A2, A9, A10, Th10;

      then (A1 \/ A3) c= L3 by XBOOLE_1: 8;

      then ( card (A1 \/ A3)) c= (k + 1) by A24, CARD_1: 11;

      then ( card (A1 \/ A3)) = (k + 1) by A22, XBOOLE_0:def 10;

      then (A1 \/ A3) = L3 by A24, A34, A25, CARD_2: 102, XBOOLE_1: 8;

      then L3 c= (L1 \/ L2) by A23, XBOOLE_1: 13;

      then (L3 \/ L4) c= (L1 \/ L2) by A31, XBOOLE_1: 8;

      then ( card (L3 \/ L4)) c= (k + 2) by A33, CARD_1: 11;

      then ( card (L3 \/ L4)) in ( succ (k + 2)) by ORDINAL1: 22;

      then ( card (L3 \/ L4)) in ( Segm ((k + 1) + 1)) or ( card (L3 \/ L4)) = (k + 2) by ORDINAL1: 8;

      then ( card (L3 \/ L4)) in ( succ ( Segm (k + 1))) or ( card (L3 \/ L4)) = (k + 2) by NAT_1: 38;

      then

       A35: ( card (L3 \/ L4)) c= (k + 1) or ( card (L3 \/ L4)) = (k + 2) by ORDINAL1: 22;

      (k + 1) c= ( card (L3 \/ L4)) by A24, CARD_1: 11, XBOOLE_1: 7;

      then ( card (L3 \/ L4)) = ((k + 1) + (2 * 0 )) or ( card (L3 \/ L4)) = (k + (2 * 1)) by A35, XBOOLE_0:def 10;

      then k c= ( card (L3 /\ L4)) by A24, A28, A1, Th2;

      then

      consider B6 be set such that

       A36: B6 c= (L3 /\ L4) and

       A37: ( card B6) = k by CARD_FIL: 36;

      

       A38: (L3 /\ L4) c= L3 by XBOOLE_1: 17;

      then (L3 /\ L4) c= X by A24, XBOOLE_1: 1;

      then

      reconsider A6 = B6 as Subset of X by A36, XBOOLE_1: 1;

      

       A39: A6 in the Points of ( G_ (k,X)) by A3, A37;

      (L3 /\ L4) c= L4 by XBOOLE_1: 17;

      then

       A40: B6 c= L4 by A36;

      reconsider A6 as POINT of ( G_ (k,X)) by A39;

      take B6;

      A6 c= B6 & B6 c= L3 by A36, A38;

      hence thesis by A2, A40, Th10;

    end;

    theorem :: COMBGRAS:12

    

     Th12: for k be Element of NAT holds for X be non empty set st 0 < k & (k + 1) c= ( card X) holds for A1,A2,A3,A4,A5,A6 be POINT of ( G_ (k,X)) holds for L1,L2,L3,L4 be LINE of ( G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds ex A6 be POINT of ( G_ (k,X)) st A6 on L3 & A6 on L4 & A6 = ((A1 /\ A2) \/ (A3 /\ A4))

    proof

      let k be Element of NAT ;

      let X be non empty set;

      assume that

       A1: 0 < k and

       A2: (k + 1) c= ( card X);

      

       A3: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A1, A2, Def1;

      

       A4: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, A2, Def1;

      let A1,A2,A3,A4,A5,A6 be POINT of ( G_ (k,X)), L1,L2,L3,L4 be LINE of ( G_ (k,X));

      assume that

       A5: A1 on L1 and

       A6: A2 on L1 and

       A7: A3 on L2 and

       A8: A4 on L2 and

       A9: A5 on L1 and

       A10: A5 on L2 and

       A11: A1 on L3 and

       A12: A3 on L3 and

       A13: A2 on L4 and

       A14: A4 on L4 and

       A15: not A5 on L3 and

       A16: not A5 on L4 and

       A17: L1 <> L2 and

       A18: L3 <> L4;

      

       A19: A1 c= L1 & A2 c= L1 by A1, A2, A5, A6, Th10;

      

       A20: A3 c= L2 & A4 c= L2 by A1, A2, A7, A8, Th10;

      

       A21: A5 c= L1 & A5 c= L2 by A1, A2, A9, A10, Th10;

      A5 in the Points of ( G_ (k,X));

      then

       A22: ex B5 be Subset of X st B5 = A5 & ( card B5) = k by A3;

      A2 in the Points of ( G_ (k,X));

      then

       A23: ex B2 be Subset of X st B2 = A2 & ( card B2) = k by A3;

      then

       A24: A2 is finite;

      reconsider k1 = (k - 1) as Element of NAT by A1, NAT_1: 20;

      L3 in the Lines of ( G_ (k,X));

      then

       A25: ex K3 be Subset of X st K3 = L3 & ( card K3) = (k + 1) by A4;

      then

       A26: L3 is finite;

      L4 in the Lines of ( G_ (k,X));

      then ex K4 be Subset of X st K4 = L4 & ( card K4) = (k + 1) by A4;

      then ( card (L3 /\ L4)) in ( Segm (k + 1)) by A25, A18, Th1;

      then ( card (L3 /\ L4)) in ( succ ( Segm k)) by NAT_1: 38;

      then

       A27: ( card (L3 /\ L4)) c= k by ORDINAL1: 22;

      A1 in the Points of ( G_ (k,X));

      then

       A28: ex B1 be Subset of X st B1 = A1 & ( card B1) = k by A3;

      then

       A29: A1 is finite;

      ( G_ (k,X)) is Vebleian by A1, A2, Th11;

      then

      consider A6 be POINT of ( G_ (k,X)) such that

       A30: A6 on L3 and

       A31: A6 on L4 by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17;

      A6 in the Points of ( G_ (k,X));

      then

       A32: ex a6 be Subset of X st a6 = A6 & ( card a6) = k by A3;

      then

       A33: A6 is finite;

      

       A34: A6 c= L3 & A6 c= L4 by A1, A2, A30, A31, Th10;

      then A6 c= (L3 /\ L4) by XBOOLE_1: 19;

      then k c= ( card (L3 /\ L4)) by A32, CARD_1: 11;

      then ( card (L3 /\ L4)) = k by A27, XBOOLE_0:def 10;

      then

       A35: (L3 /\ L4) = A6 by A32, A34, A26, CARD_2: 102, XBOOLE_1: 19;

      L2 in the Lines of ( G_ (k,X));

      then

       A36: ex K2 be Subset of X st K2 = L2 & ( card K2) = (k + 1) by A4;

      then

       A37: L2 is finite;

      A4 in the Points of ( G_ (k,X));

      then

       A38: ex B4 be Subset of X st B4 = A4 & ( card B4) = k by A3;

      then

       A39: A4 is finite;

      L1 in the Lines of ( G_ (k,X));

      then

       A40: ex K1 be Subset of X st K1 = L1 & ( card K1) = (k + 1) by A4;

      then

       A41: L1 is finite;

      A3 in the Points of ( G_ (k,X));

      then

       A42: ex B3 be Subset of X st B3 = A3 & ( card B3) = k by A3;

      then

       A43: A3 is finite;

      

       A44: A3 c= L3 & A4 c= L4 by A1, A2, A12, A14, Th10;

      then

       A45: (A3 /\ A4) c= A6 by A35, XBOOLE_1: 27;

      

       A46: A1 c= L3 & A2 c= L4 by A1, A2, A11, A13, Th10;

      then

       A47: (A1 /\ A2) c= A6 by A35, XBOOLE_1: 27;

      then

       A48: ((A1 /\ A2) \/ (A3 /\ A4)) c= A6 by A45, XBOOLE_1: 8;

      

       A49: not A6 on L1 implies A6 = ((A1 /\ A2) \/ (A3 /\ A4))

      proof

        assume

         A50: not A6 on L1;

        

         A51: not A6 on L2 implies A6 = ((A1 /\ A2) \/ (A3 /\ A4))

        proof

          

           A52: (A1 \/ A2) c= L1 by A19, XBOOLE_1: 8;

          then

           A53: ( card (A1 \/ A2)) c= (k + 1) by A40, CARD_1: 11;

          

           A54: (A3 \/ A4) c= L2 by A20, XBOOLE_1: 8;

          then

           A55: ( card (A3 \/ A4)) c= (k + 1) by A36, CARD_1: 11;

          

           A56: ( card A3) = ((k - 1) + 1) by A42;

          ( card ((A1 /\ A2) \/ (A3 /\ A4))) c= k by A32, A48, CARD_1: 11;

          then ( card ((A1 /\ A2) \/ (A3 /\ A4))) in ( succ k) by ORDINAL1: 22;

          then ( card ((A1 /\ A2) \/ (A3 /\ A4))) in ( Segm (k1 + 1)) or ( card ((A1 /\ A2) \/ (A3 /\ A4))) = k by ORDINAL1: 8;

          then ( card ((A1 /\ A2) \/ (A3 /\ A4))) in ( succ ( Segm k1)) or ( card ((A1 /\ A2) \/ (A3 /\ A4))) = k by NAT_1: 38;

          then

           A57: ( card ((A1 /\ A2) \/ (A3 /\ A4))) c= ( Segm k1) or ( card ((A1 /\ A2) \/ (A3 /\ A4))) = k by ORDINAL1: 22;

          

           A58: ( card A1) = ((k - 1) + 1) by A28;

          assume

           A59: not A6 on L2;

          

           A60: A1 <> A2 & A3 <> A4

          proof

            assume A1 = A2 or A3 = A4;

            then {A1, A6} on L3 & {A1, A6} on L4 or {A3, A6} on L3 & {A3, A6} on L4 by A11, A12, A13, A14, A30, A31, INCSP_1: 1;

            hence contradiction by A5, A7, A18, A50, A59, INCSP_1:def 10;

          end;

          then (k + 1) c= ( card (A1 \/ A2)) by A28, A23, Th1;

          then ( card (A1 \/ A2)) = (k1 + (2 * 1)) by A53, XBOOLE_0:def 10;

          then

           A61: ( card (A1 /\ A2)) = k1 by A23, A58, Th2;

          (k + 1) c= ( card (A3 \/ A4)) by A42, A38, A60, Th1;

          then ( card (A3 \/ A4)) = (k1 + (2 * 1)) by A55, XBOOLE_0:def 10;

          then

           A62: ( card (A3 /\ A4)) = k1 by A38, A56, Th2;

          

           A63: not ( card ((A1 /\ A2) \/ (A3 /\ A4))) = (k - 1)

          proof

            

             A64: A5 c= (L1 /\ L2) by A21, XBOOLE_1: 19;

            

             A65: ((A1 /\ A2) /\ (A3 /\ A4)) c= (A1 /\ A2) by XBOOLE_1: 17;

            

             A66: (((A1 /\ A2) /\ A3) /\ A4) = ((A1 /\ A2) /\ (A3 /\ A4)) by XBOOLE_1: 16;

            

             A67: (A1 /\ A2) c= A1 by XBOOLE_1: 17;

            then

             A68: A1 = ((((A1 /\ A2) /\ A3) /\ A4) \/ (A1 \ (((A1 /\ A2) /\ A3) /\ A4))) by A65, A66, XBOOLE_1: 1, XBOOLE_1: 45;

            assume

             A69: ( card ((A1 /\ A2) \/ (A3 /\ A4))) = (k - 1);

            then ( card ((A1 /\ A2) \/ (A3 /\ A4))) = (k1 + (2 * 0 ));

            then

             A70: ( card ((A1 /\ A2) /\ (A3 /\ A4))) = k1 by A61, A62, Th2;

            then

             A71: ((A1 /\ A2) /\ (A3 /\ A4)) = ((A1 /\ A2) \/ (A3 /\ A4)) by A29, A43, A69, CARD_2: 102, XBOOLE_1: 29;

            then ( card (A1 \ (((A1 /\ A2) /\ A3) /\ A4))) = (k - (k - 1)) by A28, A29, A69, A67, A65, A66, CARD_2: 44, XBOOLE_1: 1;

            then

            consider x1 be object such that

             A72: (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) = {x1} by CARD_2: 42;

            

             A73: (A1 /\ A2) c= A2 by XBOOLE_1: 17;

            then

             A74: A2 = ((((A1 /\ A2) /\ A3) /\ A4) \/ (A2 \ (((A1 /\ A2) /\ A3) /\ A4))) by A65, A66, XBOOLE_1: 1, XBOOLE_1: 45;

            ( card (A2 \ (((A1 /\ A2) /\ A3) /\ A4))) = (k - (k - 1)) by A23, A24, A69, A73, A65, A71, A66, CARD_2: 44, XBOOLE_1: 1;

            then

            consider x2 be object such that

             A75: (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) = {x2} by CARD_2: 42;

            x1 in {x1} by TARSKI:def 1;

            then

             A76: not x1 in (((A1 /\ A2) /\ A3) /\ A4) by A72, XBOOLE_0:def 5;

            

             A77: ((A1 /\ A2) /\ (A3 /\ A4)) c= (A3 /\ A4) by XBOOLE_1: 17;

            

             A78: (A3 /\ A4) c= A4 by XBOOLE_1: 17;

            then

             A79: A4 = ((((A1 /\ A2) /\ A3) /\ A4) \/ (A4 \ (((A1 /\ A2) /\ A3) /\ A4))) by A77, A66, XBOOLE_1: 1, XBOOLE_1: 45;

            ( card (A4 \ (((A1 /\ A2) /\ A3) /\ A4))) = (k - (k - 1)) by A38, A39, A69, A78, A77, A71, A66, CARD_2: 44, XBOOLE_1: 1;

            then

            consider x4 be object such that

             A80: (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) = {x4} by CARD_2: 42;

            

             A81: (A3 /\ A4) c= A3 by XBOOLE_1: 17;

            then

             A82: A3 = ((((A1 /\ A2) /\ A3) /\ A4) \/ (A3 \ (((A1 /\ A2) /\ A3) /\ A4))) by A77, A66, XBOOLE_1: 1, XBOOLE_1: 45;

            ( card (A3 \ (((A1 /\ A2) /\ A3) /\ A4))) = (k - (k - 1)) by A42, A43, A69, A81, A77, A71, A66, CARD_2: 44, XBOOLE_1: 1;

            then

            consider x3 be object such that

             A83: (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) = {x3} by CARD_2: 42;

            (k + 1) c= ( card (A3 \/ A4)) & ( card (A3 \/ A4)) c= (k + 1) by A42, A38, A36, A60, A54, Th1, CARD_1: 11;

            then ( card (A3 \/ A4)) = (k + 1) by XBOOLE_0:def 10;

            then (A3 \/ A4) = L2 by A36, A20, A37, CARD_2: 102, XBOOLE_1: 8;

            then

             A84: L2 = ((((A1 /\ A2) /\ A3) /\ A4) \/ ( {x3} \/ {x4})) by A83, A80, A82, A79, XBOOLE_1: 5;

            then

             A85: L2 = ((((A1 /\ A2) /\ A3) /\ A4) \/ {x3, x4}) by ENUMSET1: 1;

            

             A86: x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4

            proof

              assume x1 = x3 or x1 = x4 or x2 = x3 or x2 = x4;

              then {A1, A5} on L1 & {A1, A5} on L2 or {A1, A5} on L1 & {A1, A5} on L2 or {A2, A5} on L1 & {A2, A5} on L2 or {A2, A5} on L1 & {A2, A5} on L2 by A5, A6, A7, A8, A9, A10, A72, A75, A83, A80, A68, A74, A82, A79, INCSP_1: 1;

              hence contradiction by A11, A13, A15, A16, A17, INCSP_1:def 10;

            end;

            x2 in {x2} by TARSKI:def 1;

            then

             A87: not x2 in (((A1 /\ A2) /\ A3) /\ A4) by A75, XBOOLE_0:def 5;

            (k + 1) c= ( card (A1 \/ A2)) & ( card (A1 \/ A2)) c= (k + 1) by A28, A23, A40, A60, A52, Th1, CARD_1: 11;

            then ( card (A1 \/ A2)) = (k + 1) by XBOOLE_0:def 10;

            then (A1 \/ A2) = L1 by A40, A19, A41, CARD_2: 102, XBOOLE_1: 8;

            then

             A88: L1 = ((((A1 /\ A2) /\ A3) /\ A4) \/ ( {x1} \/ {x2})) by A72, A75, A68, A74, XBOOLE_1: 5;

            then

             A89: L1 = ((((A1 /\ A2) /\ A3) /\ A4) \/ {x1, x2}) by ENUMSET1: 1;

            

             A90: (L1 /\ L2) c= (((A1 /\ A2) /\ A3) /\ A4)

            proof

              assume not (L1 /\ L2) c= (((A1 /\ A2) /\ A3) /\ A4);

              then

              consider x be object such that

               A91: x in (L1 /\ L2) and

               A92: not x in (((A1 /\ A2) /\ A3) /\ A4);

              x in L1 by A91, XBOOLE_0:def 4;

              then

               A93: x in {x1, x2} by A89, A92, XBOOLE_0:def 3;

              x in L2 by A91, XBOOLE_0:def 4;

              then x1 in L2 or x2 in L2 by A93, TARSKI:def 2;

              then x1 in {x3, x4} or x2 in {x3, x4} by A85, A76, A87, XBOOLE_0:def 3;

              hence contradiction by A86, TARSKI:def 2;

            end;

            

             A94: (((A1 /\ A2) /\ A3) /\ A4) c= L2 by A84, XBOOLE_1: 10;

            (((A1 /\ A2) /\ A3) /\ A4) c= L1 by A88, XBOOLE_1: 10;

            then (((A1 /\ A2) /\ A3) /\ A4) c= (L1 /\ L2) by A94, XBOOLE_1: 19;

            then (L1 /\ L2) = (((A1 /\ A2) /\ A3) /\ A4) by A90, XBOOLE_0:def 10;

            then ( card ( Segm k)) c= ( card ( Segm k1)) by A22, A70, A66, A64, CARD_1: 11;

            then

             A95: k <= k1 by NAT_1: 40;

            k1 <= (k1 + 1) by NAT_1: 11;

            then k = (k - 1) by A95, XXREAL_0: 1;

            hence contradiction;

          end;

          (k - 1) c= ( card ((A1 /\ A2) \/ (A3 /\ A4))) by A61, CARD_1: 11, XBOOLE_1: 7;

          then ( card ((A1 /\ A2) \/ (A3 /\ A4))) = k by A57, A63, XBOOLE_0:def 10;

          hence thesis by A32, A33, A47, A45, CARD_2: 102, XBOOLE_1: 8;

        end;

        A6 on L2 implies A6 = ((A1 /\ A2) \/ (A3 /\ A4))

        proof

          assume

           A96: A6 on L2;

          

           A97: A4 = A6

          proof

            assume

             A98: A4 <> A6;

             {A4, A6} on L2 & {A4, A6} on L4 by A8, A14, A31, A96, INCSP_1: 1;

            hence contradiction by A10, A16, A98, INCSP_1:def 10;

          end;

          A3 = A6

          proof

            assume

             A99: A3 <> A6;

             {A3, A6} on L2 & {A3, A6} on L3 by A7, A12, A30, A96, INCSP_1: 1;

            hence contradiction by A10, A15, A99, INCSP_1:def 10;

          end;

          hence thesis by A46, A35, A97, XBOOLE_1: 12, XBOOLE_1: 27;

        end;

        hence thesis by A51;

      end;

      A6 on L1 implies A6 = ((A1 /\ A2) \/ (A3 /\ A4))

      proof

        assume

         A100: A6 on L1;

        

         A101: A1 = A6

        proof

          assume

           A102: A1 <> A6;

           {A1, A6} on L1 & {A1, A6} on L3 by A5, A11, A30, A100, INCSP_1: 1;

          hence contradiction by A9, A15, A102, INCSP_1:def 10;

        end;

        A2 = A6

        proof

          assume

           A103: A2 <> A6;

           {A2, A6} on L1 & {A2, A6} on L4 by A6, A13, A31, A100, INCSP_1: 1;

          hence contradiction by A9, A16, A103, INCSP_1:def 10;

        end;

        hence thesis by A44, A35, A101, XBOOLE_1: 12, XBOOLE_1: 27;

      end;

      hence thesis by A30, A31, A49;

    end;

    theorem :: COMBGRAS:13

    for k be Element of NAT holds for X be non empty set st 0 < k & (k + 1) c= ( card X) holds ( G_ (k,X)) is Desarguesian

    proof

      let k be Element of NAT ;

      let X be non empty set;

      assume that

       A1: 0 < k and

       A2: (k + 1) c= ( card X);

      let o,b1,a1,b2,a2,b3,a3,r,s,t be POINT of ( G_ (k,X));

      let C1,C2,C3,A1,A2,A3,B1,B2,B3 be LINE of ( G_ (k,X));

      assume that

       A3: {o, b1, a1} on C1 and

       A4: {o, a2, b2} on C2 and

       A5: {o, a3, b3} on C3 and

       A6: {a3, a2, t} on A1 and

       A7: {a3, r, a1} on A2 and

       A8: {a2, s, a1} on A3 and

       A9: {t, b2, b3} on B1 and

       A10: {b1, r, b3} on B2 and

       A11: {b1, s, b2} on B3 and

       A12: (C1,C2,C3) are_mutually_distinct and

       A13: o <> a1 and

       A14: o <> a2 & o <> a3 and

       A15: o <> b1 and

       A16: o <> b2 & o <> b3 and

       A17: a1 <> b1 and

       A18: a2 <> b2 and

       A19: a3 <> b3;

      

       A20: o on C1 by A3, INCSP_1: 2;

      

       A21: b2 on C2 by A4, INCSP_1: 2;

      then

       A22: b2 c= C2 by A1, A2, Th10;

      

       A23: a2 on C2 by A4, INCSP_1: 2;

      then

       A24: {a2, b2} on C2 by A21, INCSP_1: 1;

      

       A25: o on C2 by A4, INCSP_1: 2;

      then

       A26: {o, b2} on C2 by A21, INCSP_1: 1;

      

       A27: {o, a2} on C2 by A25, A23, INCSP_1: 1;

      

       A28: a3 on A1 & a2 on A1 by A6, INCSP_1: 2;

      

       A29: b3 on B2 by A10, INCSP_1: 2;

      

       A30: b3 on C3 by A5, INCSP_1: 2;

      then

       A31: b3 c= C3 by A1, A2, Th10;

      

       A32: a3 on C3 by A5, INCSP_1: 2;

      then

       A33: {a3, b3} on C3 by A30, INCSP_1: 1;

      

       A34: o on C3 by A5, INCSP_1: 2;

      then

       A35: {o, b3} on C3 by A30, INCSP_1: 1;

      

       A36: {o, a3} on C3 by A34, A32, INCSP_1: 1;

      

       A37: a3 on A2 & a1 on A2 by A7, INCSP_1: 2;

      

       A38: b1 on B3 by A11, INCSP_1: 2;

      

       A39: C1 <> C3 by A12, ZFMISC_1:def 5;

      

       A40: b1 on B2 by A10, INCSP_1: 2;

      

       A41: C2 <> C3 by A12, ZFMISC_1:def 5;

      

       A42: b3 on B1 by A9, INCSP_1: 2;

      

       A43: C1 <> C2 by A12, ZFMISC_1:def 5;

      

       A44: b2 on B1 by A9, INCSP_1: 2;

      

       A45: a1 on C1 by A3, INCSP_1: 2;

      then

       A46: a1 c= C1 by A1, A2, Th10;

      

       A47: b1 on C1 by A3, INCSP_1: 2;

      then

       A48: {o, b1} on C1 by A20, INCSP_1: 1;

      

       A49: b2 on B3 by A11, INCSP_1: 2;

      

       A50: {a1, b1} on C1 by A47, A45, INCSP_1: 1;

      

       A51: not a1 on B2 & not a2 on B3 & not a3 on B1

      proof

        assume a1 on B2 or a2 on B3 or a3 on B1;

        then {a1, b1} on B2 or {a2, b2} on B3 or {a3, b3} on B1 by A42, A40, A49, INCSP_1: 1;

        then b3 on C1 or b1 on C2 or b2 on C3 by A17, A18, A19, A44, A29, A38, A50, A24, A33, INCSP_1:def 10;

        then {o, b3} on C1 or {o, b1} on C2 or {o, b2} on C3 by A20, A25, A34, INCSP_1: 1;

        hence contradiction by A15, A16, A48, A26, A35, A43, A41, A39, INCSP_1:def 10;

      end;

      

       A52: s on A3 & s on B3 by A8, A11, INCSP_1: 2;

      

       A53: t on B1 by A9, INCSP_1: 2;

      

       A54: r on A2 & r on B2 by A7, A10, INCSP_1: 2;

      

       A55: t on A1 by A6, INCSP_1: 2;

      

       A56: a1 on A3 by A8, INCSP_1: 2;

      

       A57: a2 on A3 by A8, INCSP_1: 2;

      

       A58: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, A2, Def1;

      

       A59: {o, a1} on C1 by A20, A45, INCSP_1: 1;

      

       A60: not o on A1 & not o on B1 & not o on A2 & not o on B2 & not o on A3 & not o on B3

      proof

        assume o on A1 or o on B1 or o on A2 or o on B2 or o on A3 or o on B3;

        then {o, a2} on A1 & {o, a3} on A1 or {o, b2} on B1 & {o, b3} on B1 or {o, a1} on A2 & {o, a3} on A2 or {o, b1} on B2 & {o, b3} on B2 or {o, a2} on A3 & {o, a1} on A3 or {o, b2} on B3 & {o, b1} on B3 by A28, A37, A57, A56, A44, A42, A40, A29, A38, A49, INCSP_1: 1;

        then A1 = C2 & A1 = C3 or B1 = C2 & B1 = C3 or A2 = C1 & A2 = C3 or B2 = C1 & B2 = C3 or A3 = C2 & A3 = C1 or B3 = C2 & B3 = C1 by A13, A14, A15, A16, A59, A27, A36, A48, A26, A35, INCSP_1:def 10;

        hence contradiction by A12, ZFMISC_1:def 5;

      end;

      then

      consider salpha be POINT of ( G_ (k,X)) such that

       A61: salpha on A3 & salpha on B3 and

       A62: salpha = ((a1 /\ b1) \/ (a2 /\ b2)) by A1, A2, A20, A47, A45, A25, A23, A21, A57, A56, A38, A49, A43, A51, Th12;

      consider ralpha be POINT of ( G_ (k,X)) such that

       A63: ralpha on B2 & ralpha on A2 and

       A64: ralpha = ((a1 /\ b1) \/ (a3 /\ b3)) by A1, A2, A20, A47, A45, A34, A32, A30, A37, A40, A29, A39, A51, A60, Th12;

      

       A65: (((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2)) = ((a1 /\ b1) \/ ((a3 /\ b3) \/ (a2 /\ b2))) by XBOOLE_1: 4;

      consider talpha be POINT of ( G_ (k,X)) such that

       A66: talpha on A1 & talpha on B1 and

       A67: talpha = ((a2 /\ b2) \/ (a3 /\ b3)) by A1, A2, A25, A23, A21, A34, A32, A30, A28, A44, A42, A41, A51, A60, Th12;

      

       A68: A1 <> B1 & A2 <> B2 by A6, A7, A51, INCSP_1: 2;

      

       A69: r = ralpha & s = salpha & t = talpha

      proof

        

         A70: {s, salpha} on A3 & {s, salpha} on B3 by A52, A61, INCSP_1: 1;

        

         A71: {r, ralpha} on A2 & {r, ralpha} on B2 by A54, A63, INCSP_1: 1;

        assume

         A72: r <> ralpha or s <> salpha or t <> talpha;

         {t, talpha} on A1 & {t, talpha} on B1 by A55, A53, A66, INCSP_1: 1;

        hence contradiction by A57, A51, A68, A72, A71, A70, INCSP_1:def 10;

      end;

      then (r \/ s) = ((((a3 /\ b3) \/ (a1 /\ b1)) \/ (a1 /\ b1)) \/ (a2 /\ b2)) by A62, A64, XBOOLE_1: 4;

      then (r \/ s) = (((a3 /\ b3) \/ ((a1 /\ b1) \/ (a1 /\ b1))) \/ (a2 /\ b2)) by XBOOLE_1: 4;

      then

       A73: ((r \/ s) \/ t) = (((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2)) by A67, A69, A65, XBOOLE_1: 7, XBOOLE_1: 12;

      a2 c= C2 by A1, A2, A23, Th10;

      then

       A74: (a2 \/ b2) c= C2 by A22, XBOOLE_1: 8;

      r c= (r \/ (s \/ t)) by XBOOLE_1: 7;

      then

       A75: r c= ((r \/ s) \/ t) by XBOOLE_1: 4;

      C1 in the Lines of ( G_ (k,X));

      then

      consider C11 be Subset of X such that

       A76: C11 = C1 & ( card C11) = (k + 1) by A58;

      reconsider C1 as finite set by A76;

      

       A77: b1 c= C1 by A1, A2, A47, Th10;

      then (a1 \/ b1) c= C1 by A46, XBOOLE_1: 8;

      then

       A78: ( card (a1 \/ b1)) c= (k + 1) by A76, CARD_1: 11;

      

       A79: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A1, A2, Def1;

      o in the Points of ( G_ (k,X));

      then

       A80: ex o1 be Subset of X st o1 = o & ( card o1) = k by A79;

      b1 in the Points of ( G_ (k,X));

      then

       A81: ex b11 be Subset of X st b11 = b1 & ( card b11) = k by A79;

      a3 in the Points of ( G_ (k,X));

      then

       A82: ex a13 be Subset of X st a13 = a3 & ( card a13) = k by A79;

      then

       A83: ( card a3) = ((k - 1) + 1);

      t in the Points of ( G_ (k,X));

      then

       A84: ex t1 be Subset of X st t1 = t & ( card t1) = k by A79;

      then

       A85: t is finite;

      a2 in the Points of ( G_ (k,X));

      then

       A86: ex a12 be Subset of X st a12 = a2 & ( card a12) = k by A79;

      then

       A87: ( card a2) = ((k - 1) + 1);

      s in the Points of ( G_ (k,X));

      then

       A88: ex s1 be Subset of X st s1 = s & ( card s1) = k by A79;

      then

       A89: s is finite;

      a1 in the Points of ( G_ (k,X));

      then

       A90: ex a11 be Subset of X st a11 = a1 & ( card a11) = k by A79;

      then (k + 1) c= ( card (a1 \/ b1)) by A81, A17, Th1;

      then

       A91: ( card (a1 \/ b1)) = ((k - 1) + (2 * 1)) by A78, XBOOLE_0:def 10;

      

       A92: (k - 1) is Element of NAT by A1, NAT_1: 20;

      C2 in the Lines of ( G_ (k,X));

      then ex C12 be Subset of X st C12 = C2 & ( card C12) = (k + 1) by A58;

      then

       A93: ( card (a2 \/ b2)) c= (k + 1) by A74, CARD_1: 11;

      b2 in the Points of ( G_ (k,X));

      then

       A94: ex b12 be Subset of X st b12 = b2 & ( card b12) = k by A79;

      then (k + 1) c= ( card (a2 \/ b2)) by A86, A18, Th1;

      then

       A95: ( card (a2 \/ b2)) = ((k - 1) + (2 * 1)) by A93, XBOOLE_0:def 10;

      then

       A96: ( card (a2 /\ b2)) = (k - 1) by A92, A94, A87, Th2;

      

       A97: ( card (a2 /\ b2)) = ((k - 2) + 1) by A92, A94, A95, A87, Th2;

      

       A98: ( card a1) = ((k - 1) + 1) by A90;

      then

       A99: ( card (a1 /\ b1)) = (k - 1) by A92, A81, A91, Th2;

      a3 c= C3 by A1, A2, A32, Th10;

      then

       A100: (a3 \/ b3) c= C3 by A31, XBOOLE_1: 8;

      s c= (s \/ (r \/ t)) by XBOOLE_1: 7;

      then

       A101: s c= ((r \/ s) \/ t) by XBOOLE_1: 4;

      ( 0 + 1) < (k + 1) by A1, XREAL_1: 8;

      then 1 <= ((k - 1) + 1) by NAT_1: 13;

      then 1 <= (k - 1) or k = 1 by A92, NAT_1: 8;

      then

       A102: (1 + 1) <= ((k - 1) + 1) or k = 1 by XREAL_1: 6;

      

       A103: o c= C1 by A1, A2, A20, Th10;

      

       A104: not k = 1

      proof

        assume

         A105: k = 1;

        then

        consider z1 be object such that

         A106: o = {z1} by A80, CARD_2: 42;

        consider z3 be object such that

         A107: b1 = {z3} by A81, A105, CARD_2: 42;

        consider z2 be object such that

         A108: a1 = {z2} by A90, A105, CARD_2: 42;

        (o \/ a1) c= C1 by A103, A46, XBOOLE_1: 8;

        then ((o \/ a1) \/ b1) c= C1 by A77, XBOOLE_1: 8;

        then ( {z1, z2} \/ b1) c= C1 by A106, A108, ENUMSET1: 1;

        then

         A109: {z1, z2, z3} c= C1 by A107, ENUMSET1: 3;

        ( card {z1, z2, z3}) = 3 by A13, A15, A17, A106, A108, A107, CARD_2: 58;

        then ( Segm 3) c= ( Segm ( card C1)) by A109, CARD_1: 11;

        hence contradiction by A76, A105, NAT_1: 39;

      end;

      then

       A110: (k - 2) is Element of NAT by A102, NAT_1: 21;

      C3 in the Lines of ( G_ (k,X));

      then ex C13 be Subset of X st C13 = C3 & ( card C13) = (k + 1) by A58;

      then

       A111: ( card (a3 \/ b3)) c= (k + 1) by A100, CARD_1: 11;

      b3 in the Points of ( G_ (k,X));

      then

       A112: ex b13 be Subset of X st b13 = b3 & ( card b13) = k by A79;

      then (k + 1) c= ( card (a3 \/ b3)) by A82, A19, Th1;

      then

       A113: ( card (a3 \/ b3)) = ((k - 1) + (2 * 1)) by A111, XBOOLE_0:def 10;

      then

       A114: ( card (a3 /\ b3)) = (k - 1) by A92, A112, A83, Th2;

      r in the Points of ( G_ (k,X));

      then

       A115: ex r1 be Subset of X st r1 = r & ( card r1) = k by A79;

      then (r \/ s) c= X by A88, XBOOLE_1: 8;

      then

       A116: ((r \/ s) \/ t) c= X by A84, XBOOLE_1: 8;

      

       A117: ( card (a3 /\ b3)) = ((k - 2) + 1) by A92, A112, A113, A83, Th2;

      

       A118: ( card (a1 /\ b1)) = ((k - 2) + 1) by A92, A81, A91, A98, Th2;

      ( card ((a1 /\ b1) \/ (a2 /\ b2))) = ((k - 2) + (2 * 1)) by A62, A69, A88;

      then

       A119: ( card ((a1 /\ b1) /\ (a2 /\ b2))) = (k - 2) by A110, A118, A97, Th2;

      ( card ((a2 /\ b2) \/ (a3 /\ b3))) = ((k - 2) + (2 * 1)) by A67, A69, A84;

      then

       A120: ( card ((a2 /\ b2) /\ (a3 /\ b3))) = (k - 2) by A110, A97, A117, Th2;

      ( card ((a1 /\ b1) \/ (a3 /\ b3))) = ((k - 2) + (2 * 1)) by A64, A69, A115;

      then

       A121: ( card ((a1 /\ b1) /\ (a3 /\ b3))) = (k - 2) by A110, A118, A117, Th2;

      

       A122: t c= ((r \/ s) \/ t) by XBOOLE_1: 7;

      

       A123: k = 2 implies ex O be LINE of ( G_ (k,X)) st {r, s, t} on O

      proof

        assume k = 2;

        then ( card ((r \/ s) \/ t)) = (k + 1) by A99, A96, A114, A73, A121, A120, A119, Th7;

        then ((r \/ s) \/ t) in the Lines of ( G_ (k,X)) by A58, A116;

        then

        consider O be LINE of ( G_ (k,X)) such that

         A124: O = ((r \/ s) \/ t);

        

         A125: t on O by A1, A2, A122, A124, Th10;

        r on O & s on O by A1, A2, A75, A101, A124, Th10;

        then {r, s, t} on O by A125, INCSP_1: 2;

        hence thesis;

      end;

      

       A126: r is finite by A115;

      

       A127: 3 <= k implies ex O be LINE of ( G_ (k,X)) st {r, s, t} on O

      proof

        

         A128: ( card ((r \/ s) \/ t)) = (k + 1) implies ex O be LINE of ( G_ (k,X)) st {r, s, t} on O

        proof

          assume ( card ((r \/ s) \/ t)) = (k + 1);

          then ((r \/ s) \/ t) in the Lines of ( G_ (k,X)) by A58, A116;

          then

          consider O be LINE of ( G_ (k,X)) such that

           A129: O = ((r \/ s) \/ t);

          

           A130: t on O by A1, A2, A122, A129, Th10;

          r on O & s on O by A1, A2, A75, A101, A129, Th10;

          then {r, s, t} on O by A130, INCSP_1: 2;

          hence thesis;

        end;

        

         A131: ( card ((r \/ s) \/ t)) = k implies ex O be LINE of ( G_ (k,X)) st {r, s, t} on O

        proof

          assume

           A132: ( card ((r \/ s) \/ t)) = k;

          then

           A133: t = ((r \/ s) \/ t) by A84, A126, A89, A85, CARD_2: 102, XBOOLE_1: 7;

          r = ((r \/ s) \/ t) & s = ((r \/ s) \/ t) by A115, A88, A126, A89, A85, A75, A101, A132, CARD_2: 102;

          then {r, s, t} on A1 by A55, A133, INCSP_1: 2;

          hence thesis;

        end;

        assume 3 <= k;

        hence thesis by A99, A96, A114, A73, A102, A121, A120, A119, A128, A131, Th7;

      end;

      k = 2 or 2 <= (k - 1) by A92, A104, A102, NAT_1: 8;

      then k = 2 or (2 + 1) <= ((k - 1) + 1) by XREAL_1: 6;

      hence thesis by A123, A127;

    end;

    definition

      let S be IncProjStr;

      let K be Subset of the Points of S;

      :: COMBGRAS:def2

      attr K is clique means for A,B be POINT of S st A in K & B in K holds ex L be LINE of S st {A, B} on L;

    end

    definition

      let S be IncProjStr;

      let K be Subset of the Points of S;

      :: COMBGRAS:def3

      attr K is maximal_clique means K is clique & for U be Subset of the Points of S st U is clique & K c= U holds U = K;

    end

    definition

      let k be Nat;

      let X be non empty set;

      let T be Subset of the Points of ( G_ (k,X));

      :: COMBGRAS:def4

      attr T is STAR means ex S be Subset of X st ( card S) = (k - 1) & T = { A where A be Subset of X : ( card A) = k & S c= A };

      :: COMBGRAS:def5

      attr T is TOP means ex S be Subset of X st ( card S) = (k + 1) & T = { A where A be Subset of X : ( card A) = k & A c= S };

    end

    theorem :: COMBGRAS:14

    

     Th14: for k be Element of NAT holds for X be non empty set st 2 <= k & (k + 2) c= ( card X) holds for K be Subset of the Points of ( G_ (k,X)) holds K is STAR or K is TOP implies K is maximal_clique

    proof

      let k be Element of NAT ;

      let X be non empty set;

      assume that

       A1: 2 <= k and

       A2: (k + 2) c= ( card X);

      

       A3: (k - 2) is Element of NAT by A1, NAT_1: 21;

      then

      reconsider k2 = (k - 2) as Nat;

      let K be Subset of the Points of ( G_ (k,X));

      

       A4: ( succ ( Segm k)) = ( Segm (k + 1)) by NAT_1: 38;

      

       A5: ( succ ( Segm (k + 1))) = ( Segm ((k + 1) + 1)) by NAT_1: 38;

      (k + 1) <= (k + 2) by XREAL_1: 7;

      then ( Segm (k + 1)) c= ( Segm (k + 2)) by NAT_1: 39;

      then

       A6: (k + 1) c= ( card X) by A2;

      then

       A7: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A1, Def1;

      

       A8: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, A6, Def1;

      reconsider k1 = (k - 1) as Element of NAT by A1, NAT_1: 21, XXREAL_0: 2;

      

       A9: ( succ ( Segm k1)) = ( Segm (k1 + 1)) by NAT_1: 38;

      

       A10: K is STAR implies K is maximal_clique

      proof

        assume K is STAR;

        then

        consider S be Subset of X such that

         A11: ( card S) = (k - 1) and

         A12: K = { A where A be Subset of X : ( card A) = k & S c= A };

        

         A13: S is finite by A1, A11, NAT_1: 21, XXREAL_0: 2;

        

         A14: for U be Subset of the Points of ( G_ (k,X)) st U is clique & K c= U holds U = K

        proof

          

           A15: ( succ ( Segm k2)) = ( Segm (k2 + 1)) by NAT_1: 38;

          let U be Subset of the Points of ( G_ (k,X));

          assume that

           A16: U is clique and

           A17: K c= U and

           A18: U <> K;

           not U c= K by A17, A18, XBOOLE_0:def 10;

          then

          consider A be object such that

           A19: A in U and

           A20: not A in K;

          reconsider A as set by TARSKI: 1;

          consider A2 be POINT of ( G_ (k,X)) such that

           A21: A2 = A by A19;

          ( card (S /\ A)) c= (k - 1) by A11, CARD_1: 11, XBOOLE_1: 17;

          then ( card (S /\ A)) in ( succ k1) by ORDINAL1: 22;

          then

           A22: ( card (S /\ A)) in ( succ (k - 2)) or ( card (S /\ A)) = (k - 1) by A15, ORDINAL1: 8;

          

           A23: (S /\ A) c= S & (S /\ A) c= A by XBOOLE_1: 17;

          A in the Points of ( G_ (k,X)) by A19;

          then

          consider A1 be Subset of X such that

           A24: A1 = A & ( card A1) = k by A7;

           not S c= A by A12, A20, A24;

          then

           A25: ( card (S /\ A)) c= (k - 2) by A3, A11, A13, A23, A22, CARD_2: 102, ORDINAL1: 22;

          

           A26: not (X \ (A \/ S)) <> {}

          proof

            

             A27: ( succ ( Segm k2)) = ( Segm (k2 + 1)) by NAT_1: 38;

            assume (X \ (A \/ S)) <> {} ;

            then

            consider y be object such that

             A28: y in (X \ (A \/ S)) by XBOOLE_0:def 1;

            

             A29: not y in (A \/ S) by A28, XBOOLE_0:def 5;

            then

             A30: not y in S by XBOOLE_0:def 3;

            then

             A31: ( card (S \/ {y})) = ((k - 1) + 1) by A11, A13, CARD_2: 41;

            

             A32: {y} c= X by A28, ZFMISC_1: 31;

            then (S \/ {y}) c= X by XBOOLE_1: 8;

            then (S \/ {y}) in the Points of ( G_ (k,X)) by A7, A31;

            then

            consider B be POINT of ( G_ (k,X)) such that

             A33: B = (S \/ {y});

            

             A34: not y in A by A29, XBOOLE_0:def 3;

            (A /\ B) c= (A /\ S)

            proof

              let a be object;

              assume

               A35: a in (A /\ B);

              then a in (S \/ {y}) by A33, XBOOLE_0:def 4;

              then

               A36: a in S or a in {y} by XBOOLE_0:def 3;

              a in A by A35, XBOOLE_0:def 4;

              hence thesis by A34, A36, TARSKI:def 1, XBOOLE_0:def 4;

            end;

            then ( card (A /\ B)) c= ( card (A /\ S)) by CARD_1: 11;

            then ( card (A /\ B)) c= (k - 2) by A25;

            then

             A37: ( card (A /\ B)) in (k - 1) by A27, ORDINAL1: 22;

            

             A38: not ex L be LINE of ( G_ (k,X)) st {A2, B} on L

            proof

              A <> B by A33, A34, XBOOLE_1: 7, ZFMISC_1: 31;

              then

               A39: (k + 1) c= ( card (A \/ B)) by A24, A31, A33, Th1;

              assume ex L be LINE of ( G_ (k,X)) st {A2, B} on L;

              then

              consider L be LINE of ( G_ (k,X)) such that

               A40: {A2, B} on L;

              B on L by A40, INCSP_1: 1;

              then

               A41: B c= L by A1, A6, Th10;

              L in the Lines of ( G_ (k,X));

              then

               A42: ex L1 be Subset of X st L = L1 & ( card L1) = (k + 1) by A8;

              A2 on L by A40, INCSP_1: 1;

              then A c= L by A1, A6, A21, Th10;

              then (A \/ B) c= L by A41, XBOOLE_1: 8;

              then ( card (A \/ B)) c= (k + 1) by A42, CARD_1: 11;

              then

               A43: ( card (A \/ B)) = ((k - 1) + (2 * 1)) by A39, XBOOLE_0:def 10;

              ( card B) = ((k - 1) + 1) by A11, A13, A30, A33, CARD_2: 41;

              then ( card (A /\ B)) = k1 by A24, A43, Th2;

              hence contradiction by A37;

            end;

            

             A44: S c= B by A33, XBOOLE_1: 7;

            B c= X by A32, A33, XBOOLE_1: 8;

            then B in K by A12, A31, A33, A44;

            hence contradiction by A16, A17, A19, A21, A38;

          end;

          k1 < (k1 + 1) by NAT_1: 13;

          then ( card S) in ( Segm k) by A11, NAT_1: 44;

          then ( card S) in ( card A) by A24;

          then (A \ S) <> {} by CARD_1: 68;

          then

          consider x be object such that

           A45: x in (A \ S) by XBOOLE_0:def 1;

           not x in S by A45, XBOOLE_0:def 5;

          then

           A46: ( card (S \/ {x})) = ((k - 1) + 1) by A11, A13, CARD_2: 41;

          

           A47: {x} c= A by A45, ZFMISC_1: 31;

          x in A by A45;

          then

           A48: {x} c= X by A24, ZFMISC_1: 31;

          then

           A49: (S \/ {x}) c= X by XBOOLE_1: 8;

           not (X \ (A \/ S)) = {}

          proof

            assume (X \ (A \/ S)) = {} ;

            then

             A50: X c= (A \/ S) by XBOOLE_1: 37;

            (S \/ {x}) in the Points of ( G_ (k,X)) by A7, A46, A49;

            then

            consider B be POINT of ( G_ (k,X)) such that

             A51: B = (S \/ {x});

            (A \/ B) = ((A \/ S) \/ {x}) by A51, XBOOLE_1: 4;

            then

             A52: (A \/ B) = (A \/ S) by A47, XBOOLE_1: 10, XBOOLE_1: 12;

            (A \/ S) c= X by A24, XBOOLE_1: 8;

            then

             A53: (A \/ S) = X by A50, XBOOLE_0:def 10;

            

             A54: not ex L be LINE of ( G_ (k,X)) st {A2, B} on L

            proof

              assume ex L be LINE of ( G_ (k,X)) st {A2, B} on L;

              then

              consider L be LINE of ( G_ (k,X)) such that

               A55: {A2, B} on L;

              B on L by A55, INCSP_1: 1;

              then

               A56: B c= L by A1, A6, Th10;

              A2 on L by A55, INCSP_1: 1;

              then A c= L by A1, A6, A21, Th10;

              then (A \/ B) c= L by A56, XBOOLE_1: 8;

              then ( card (A \/ B)) c= ( card L) by CARD_1: 11;

              then

               A57: (k + 2) c= ( card L) by A2, A53, A52;

              L in the Lines of ( G_ (k,X));

              then ex L1 be Subset of X st L = L1 & ( card L1) = (k + 1) by A8;

              then (k + 1) in (k + 1) by A5, A57, ORDINAL1: 21;

              hence contradiction;

            end;

            S c= B & B c= X by A48, A51, XBOOLE_1: 8, XBOOLE_1: 10;

            then B in K by A12, A46, A51;

            hence contradiction by A16, A17, A19, A21, A54;

          end;

          hence thesis by A26;

        end;

        K is clique

        proof

          let A,B be POINT of ( G_ (k,X));

          assume that

           A58: A in K and

           A59: B in K;

          

           A60: ex A1 be Subset of X st A1 = A & ( card A1) = k & S c= A1 by A12, A58;

          then

           A61: A is finite;

          

           A62: ex B1 be Subset of X st B1 = B & ( card B1) = k & S c= B1 by A12, A59;

          then S c= (A /\ B) by A60, XBOOLE_1: 19;

          then (k - 1) c= ( card (A /\ B)) by A11, CARD_1: 11;

          then k1 in ( succ ( card (A /\ B))) by ORDINAL1: 22;

          then ( card (A /\ B)) = (k - 1) or (k - 1) in ( card (A /\ B)) by ORDINAL1: 8;

          then

           A63: ( card (A /\ B)) = (k - 1) or k c= ( card (A /\ B)) by A9, ORDINAL1: 21;

          

           A64: B is finite by A62;

          

           A65: ( card (A /\ B)) = k implies ex L be LINE of ( G_ (k,X)) st {A, B} on L

          proof

            

             A66: ( card A) <> ( card X)

            proof

              assume ( card A) = ( card X);

              then k in k by A6, A4, A60, ORDINAL1: 21;

              hence contradiction;

            end;

            ( card A) c= ( card X) by A60, CARD_1: 11;

            then ( card A) in ( card X) by A66, CARD_1: 3;

            then (X \ A) <> {} by CARD_1: 68;

            then

            consider x be object such that

             A67: x in (X \ A) by XBOOLE_0:def 1;

             {x} c= X by A67, ZFMISC_1: 31;

            then

             A68: (A \/ {x}) c= X by A60, XBOOLE_1: 8;

             not x in A by A67, XBOOLE_0:def 5;

            then ( card (A \/ {x})) = (k + 1) by A60, A61, CARD_2: 41;

            then (A \/ {x}) in the Lines of ( G_ (k,X)) by A8, A68;

            then

            consider L be LINE of ( G_ (k,X)) such that

             A69: L = (A \/ {x});

            assume ( card (A /\ B)) = k;

            then (A /\ B) = A & (A /\ B) = B by A60, A62, A61, A64, CARD_2: 102, XBOOLE_1: 17;

            then B c= (A \/ {x}) by XBOOLE_1: 7;

            then

             A70: B on L by A1, A6, A69, Th10;

            A c= (A \/ {x}) by XBOOLE_1: 7;

            then A on L by A1, A6, A69, Th10;

            then {A, B} on L by A70, INCSP_1: 1;

            hence thesis;

          end;

          

           A71: ( card (A /\ B)) = (k - 1) implies ex L be LINE of ( G_ (k,X)) st {A, B} on L

          proof

            

             A72: (A \/ B) c= X by A60, A62, XBOOLE_1: 8;

            assume

             A73: ( card (A /\ B)) = (k - 1);

            ( card A) = ((k - 1) + 1) by A60;

            then ( card (A \/ B)) = (k1 + (2 * 1)) by A62, A73, Th2;

            then (A \/ B) in the Lines of ( G_ (k,X)) by A8, A72;

            then

            consider L be LINE of ( G_ (k,X)) such that

             A74: L = (A \/ B);

            B c= (A \/ B) by XBOOLE_1: 7;

            then

             A75: B on L by A1, A6, A74, Th10;

            A c= (A \/ B) by XBOOLE_1: 7;

            then A on L by A1, A6, A74, Th10;

            then {A, B} on L by A75, INCSP_1: 1;

            hence thesis;

          end;

          ( card (A /\ B)) c= k by A60, CARD_1: 11, XBOOLE_1: 17;

          hence thesis by A63, A71, A65, XBOOLE_0:def 10;

        end;

        hence thesis by A14;

      end;

      

       A76: ( succ 0 ) = ( 0 + 1);

      K is TOP implies K is maximal_clique

      proof

        assume K is TOP;

        then

        consider S be Subset of X such that

         A77: ( card S) = (k + 1) and

         A78: K = { A where A be Subset of X : ( card A) = k & A c= S };

        reconsider S as finite set by A77;

        

         A79: for U be Subset of the Points of ( G_ (k,X)) st U is clique & K c= U holds U = K

        proof

          

           A80: (k - 2) <= ((k - 2) + 1) by A3, NAT_1: 11;

          let U be Subset of the Points of ( G_ (k,X));

          assume that

           A81: U is clique and

           A82: K c= U and

           A83: U <> K;

           not U c= K by A82, A83, XBOOLE_0:def 10;

          then

          consider A be object such that

           A84: A in U and

           A85: not A in K;

          reconsider A as set by TARSKI: 1;

          consider A2 be POINT of ( G_ (k,X)) such that

           A86: A2 = A by A84;

          A in the Points of ( G_ (k,X)) by A84;

          then

           A87: ex A1 be Subset of X st A1 = A & ( card A1) = k by A7;

          then

          reconsider A as finite set;

          

           A88: ( card A) <> ( card S) by A77, A87;

          

           A89: not A c= S by A78, A85, A87;

          then

          consider x be object such that

           A90: x in A and

           A91: not x in S;

          k <= (k + 1) by NAT_1: 11;

          then ( Segm ( card A)) c= ( Segm ( card S)) by A77, A87, NAT_1: 39;

          then ( card A) in ( card S) by A88, CARD_1: 3;

          then

           A92: (S \ A) <> {} by CARD_1: 68;

          2 c= ( card (S \ A))

          proof

            

             A93: not ( card (S \ A)) = 1

            proof

              assume ( card (S \ A)) = 1;

              then

               A94: ( card (S \ (S \ A))) = ((k + 1) - 1) by A77, CARD_2: 44;

              (S \ (S \ A)) = (S /\ A) & (S /\ A) c= S by XBOOLE_1: 17, XBOOLE_1: 48;

              hence contradiction by A87, A89, A94, CARD_2: 102, XBOOLE_1: 17;

            end;

            assume not 2 c= ( card (S \ A));

            then ( card (S \ A)) in ( succ 1) by ORDINAL1: 16;

            then ( card (S \ A)) in 1 or ( card (S \ A)) = 1 by ORDINAL1: 8;

            then ( card (S \ A)) c= 0 or ( card (S \ A)) = 1 by A76, ORDINAL1: 22;

            hence contradiction by A92, A93;

          end;

          then

          consider B1 be set such that

           A95: B1 c= (S \ A) and

           A96: ( card B1) = 2 by CARD_FIL: 36;

          

           A97: B1 c= S by A95, XBOOLE_1: 106;

          then

           A98: not x in B1 by A91;

          ( card (S \ B1)) = ((k + 1) - 2) by A77, A95, A96, CARD_2: 44, XBOOLE_1: 106;

          then ( Segm k2) c= ( Segm ( card (S \ B1))) by A80, NAT_1: 39;

          then

          consider B2 be set such that

           A99: B2 c= (S \ B1) and

           A100: ( card B2) = (k - 2) by CARD_FIL: 36;

          

           A101: ( card (B1 \/ B2)) = (2 + (k - 2)) by A95, A96, A99, A100, CARD_2: 40, XBOOLE_1: 106;

          (S \ B1) c= X by XBOOLE_1: 1;

          then

           A102: B2 c= X by A99;

          (S \ A) c= X by XBOOLE_1: 1;

          then B1 c= X by A95;

          then

           A103: (B1 \/ B2) c= X by A102, XBOOLE_1: 8;

          then (B1 \/ B2) in the Points of ( G_ (k,X)) by A7, A101;

          then

          consider B be POINT of ( G_ (k,X)) such that

           A104: B = (B1 \/ B2);

          B1 misses A by A95, XBOOLE_1: 106;

          then

           A105: (B1 /\ A) = {} by XBOOLE_0:def 7;

          B2 c= S by A99, XBOOLE_1: 106;

          then

           A106: (B1 \/ B2) c= S by A97, XBOOLE_1: 8;

          then

           A107: not x in (B1 \/ B2) by A91;

          

           A108: (A /\ B) c= (A \/ B) by XBOOLE_1: 29;

          

           A109: (k + 2) c= ( card (A \/ B))

          proof

            

             A110: ( {x} \/ B1) misses (A /\ B)

            proof

              assume not ( {x} \/ B1) misses (A /\ B);

              then (( {x} \/ B1) /\ (A /\ B)) <> {} by XBOOLE_0:def 7;

              then

              consider y be object such that

               A111: y in (( {x} \/ B1) /\ (A /\ B)) by XBOOLE_0:def 1;

              y in (A /\ B) by A111, XBOOLE_0:def 4;

              then

               A112: y in A & y in B by XBOOLE_0:def 4;

              y in ( {x} \/ B1) by A111, XBOOLE_0:def 4;

              then y in {x} or y in B1 by XBOOLE_0:def 3;

              hence contradiction by A104, A107, A105, A112, TARSKI:def 1, XBOOLE_0:def 4;

            end;

             {x} c= A by A90, ZFMISC_1: 31;

            then {x} c= (A \/ B) by XBOOLE_1: 10;

            then

             A113: ((A /\ B) \/ {x}) c= (A \/ B) by A108, XBOOLE_1: 8;

            B1 c= B by A104, XBOOLE_1: 10;

            then B1 c= (A \/ B) by XBOOLE_1: 10;

            then (((A /\ B) \/ {x}) \/ B1) c= (A \/ B) by A113, XBOOLE_1: 8;

            then ((A /\ B) \/ ( {x} \/ B1)) c= (A \/ B) by XBOOLE_1: 4;

            then

             A114: ( card ((A /\ B) \/ ( {x} \/ B1))) c= ( card (A \/ B)) by CARD_1: 11;

            assume not (k + 2) c= ( card (A \/ B));

            then

             A115: ( card (A \/ B)) in ( succ (k + 1)) by A5, ORDINAL1: 16;

            then

             A116: ( card (A \/ B)) c= (k + 1) by ORDINAL1: 22;

            ( card (A \/ B)) = (k + 1) or ( card (A \/ B)) in ( succ k) & A c= (A \/ B) by A4, A115, ORDINAL1: 8, XBOOLE_1: 7;

            then ( card (A \/ B)) = (k + 1) or ( card (A \/ B)) c= k & k c= ( card (A \/ B)) by A87, CARD_1: 11, ORDINAL1: 22;

            then

             A117: ( card (A \/ B)) = ((k - 1) + (2 * 1)) or ( card (A \/ B)) = (k + (2 * 0 )) by XBOOLE_0:def 10;

            ( card A) = ((k - 1) + 1) by A87;

            then

             A118: ( card (A /\ B)) = k1 or ( card (A /\ B)) = k by A101, A104, A117, Th2;

            ( card ( {x} \/ B1)) = (2 + 1) by A95, A96, A98, CARD_2: 41;

            then ( card ((A /\ B) \/ ( {x} \/ B1))) = ((k - 1) + 3) or ( card ((A /\ B) \/ ( {x} \/ B1))) = (k + 3) by A95, A110, A118, CARD_2: 40;

            then ( Segm (k + 2)) c= ( Segm (k + 1)) or ( Segm (k + 3)) c= ( Segm (k + 1)) by A116, A114;

            then (k + 1) in (k + 1) or (k + 3) <= (k + 1) by A5, NAT_1: 39, ORDINAL1: 21;

            hence contradiction by XREAL_1: 6;

          end;

          

           A119: not ex L be LINE of ( G_ (k,X)) st {A2, B} on L

          proof

            assume ex L be LINE of ( G_ (k,X)) st {A2, B} on L;

            then

            consider L be LINE of ( G_ (k,X)) such that

             A120: {A2, B} on L;

            B on L by A120, INCSP_1: 1;

            then

             A121: B c= L by A1, A6, Th10;

            L in the Lines of ( G_ (k,X));

            then

             A122: ex L1 be Subset of X st L = L1 & ( card L1) = (k + 1) by A8;

            A2 on L by A120, INCSP_1: 1;

            then A c= L by A1, A6, A86, Th10;

            then (A \/ B) c= L by A121, XBOOLE_1: 8;

            then

             A123: ( card (A \/ B)) c= (k + 1) by A122, CARD_1: 11;

            (k + 2) c= (k + 1) by A109, A123;

            then (k + 1) in (k + 1) by A5, ORDINAL1: 21;

            hence contradiction;

          end;

          B in K by A78, A101, A103, A106, A104;

          hence thesis by A81, A82, A84, A86, A119;

        end;

        K is clique

        proof

          let A,B be POINT of ( G_ (k,X));

          assume that

           A124: A in K and

           A125: B in K;

          S in the Lines of ( G_ (k,X)) by A8, A77;

          then

          consider L be LINE of ( G_ (k,X)) such that

           A126: L = S;

          ex B1 be Subset of X st B1 = B & ( card B1) = k & B1 c= S by A78, A125;

          then

           A127: B on L by A1, A6, A126, Th10;

          ex A1 be Subset of X st A1 = A & ( card A1) = k & A1 c= S by A78, A124;

          then A on L by A1, A6, A126, Th10;

          then {A, B} on L by A127, INCSP_1: 1;

          hence thesis;

        end;

        hence thesis by A79;

      end;

      hence thesis by A10;

    end;

    theorem :: COMBGRAS:15

    

     Th15: for k be Element of NAT holds for X be non empty set st 2 <= k & (k + 2) c= ( card X) holds for K be Subset of the Points of ( G_ (k,X)) holds K is maximal_clique implies K is STAR or K is TOP

    proof

      

       A1: ( succ 0 ) = ( 0 + 1);

      

       A2: ( succ 2) = (2 + 1);

      let k be Element of NAT ;

      let X be non empty set;

      assume that

       A3: 2 <= k and

       A4: (k + 2) c= ( card X);

      (k + 1) <= (k + 2) by XREAL_1: 7;

      then

       A5: ( Segm (k + 1)) c= ( Segm (k + 2)) by NAT_1: 39;

      then

       A6: (k + 1) c= ( card X) by A4;

      then

       A7: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A3, Def1;

      

       A8: ( succ ( Segm (k + 1))) = ( Segm ((k + 1) + 1)) by NAT_1: 38;

      

       A9: 1 <= k by A3, XXREAL_0: 2;

      let K be Subset of the Points of ( G_ (k,X));

      

       A10: ( succ ( Segm k)) = ( Segm (k + 1)) by NAT_1: 38;

       0 c= ( card K);

      then 0 in ( succ ( card K)) by ORDINAL1: 22;

      then

       A11: ( card K) = 0 or 0 in ( card K) by ORDINAL1: 8;

      assume

       A12: K is maximal_clique;

      then

       A13: K is clique;

      

       A14: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A3, A6, Def1;

      k <= (k + 1) by NAT_1: 11;

      then

       A15: ( Segm k) c= ( Segm (k + 1)) by NAT_1: 39;

      then

       A16: k c= ( card X) by A6;

      K <> {}

      proof

        consider A1 be set such that

         A17: A1 c= X and

         A18: ( card A1) = k by A16, CARD_FIL: 36;

        A1 in the Points of ( G_ (k,X)) by A7, A17, A18;

        then

        consider A be POINT of ( G_ (k,X)) such that

         A19: A = A1;

        ( card A) <> ( card X)

        proof

          assume ( card A) = ( card X);

          then (k + 1) c= k by A4, A5, A18, A19;

          then k in k by A10, ORDINAL1: 21;

          hence contradiction;

        end;

        then ( card A) in ( card X) by A16, A18, A19, CARD_1: 3;

        then (X \ A) <> {} by CARD_1: 68;

        then

        consider x be object such that

         A20: x in (X \ A) by XBOOLE_0:def 1;

         {x} c= X by A20, ZFMISC_1: 31;

        then

         A21: (A \/ {x}) c= X by A17, A19, XBOOLE_1: 8;

        

         A22: not x in A by A20, XBOOLE_0:def 5;

        A is finite by A18, A19;

        then ( card (A \/ {x})) = (k + 1) by A18, A19, A22, CARD_2: 41;

        then (A \/ {x}) in the Lines of ( G_ (k,X)) by A14, A21;

        then

        consider L be LINE of ( G_ (k,X)) such that

         A23: L = (A \/ {x});

        consider U be Subset of the Points of ( G_ (k,X)) such that

         A24: U = {A};

        A c= L by A23, XBOOLE_1: 7;

        then

         A25: A on L by A3, A6, Th10;

        

         A26: U is clique

        proof

          let B,C be POINT of ( G_ (k,X));

          assume B in U & C in U;

          then B on L & C on L by A25, A24, TARSKI:def 1;

          then {B, C} on L by INCSP_1: 1;

          hence thesis;

        end;

        assume

         A27: K = {} ;

        then K c= U;

        hence contradiction by A12, A27, A24, A26;

      end;

      then 1 c= ( card K) by A1, A11, ORDINAL1: 21;

      then 1 in ( succ ( card K)) by ORDINAL1: 22;

      then

       A28: ( card K) = 1 or 1 in ( card K) by ORDINAL1: 8;

      

       A29: (k - 1) is Element of NAT by A3, NAT_1: 21, XXREAL_0: 2;

      then

      reconsider k1 = (k - 1) as Nat;

      

       A30: ( card K) <> 1

      proof

        assume ( card K) = 1;

        then

        consider A3 be object such that

         A31: K = {A3} by CARD_2: 42;

        

         A32: A3 in K by A31, TARSKI:def 1;

        then

        consider A be POINT of ( G_ (k,X)) such that

         A33: A = A3;

        A3 in the Points of ( G_ (k,X)) by A32;

        then

         A34: ex A4 be Subset of X st A = A4 & ( card A4) = k by A7, A33;

        then

        reconsider AA = A as finite set;

        

         A35: A is finite by A34;

        

         A36: ( card A) <> ( card X)

        proof

          assume ( card A) = ( card X);

          then (k + 1) c= k by A4, A5, A34;

          then k in k by A10, ORDINAL1: 21;

          hence contradiction;

        end;

        ( card A) c= ( card X) by A6, A15, A34;

        then ( card A) in ( card X) by A36, CARD_1: 3;

        then (X \ A) <> {} by CARD_1: 68;

        then

        consider x be object such that

         A37: x in (X \ A) by XBOOLE_0:def 1;

        

         A38: {x} c= X by A37, ZFMISC_1: 31;

        then

         A39: (A \/ {x}) c= X by A34, XBOOLE_1: 8;

         not x in A by A37, XBOOLE_0:def 5;

        then ( card (A \/ {x})) = (k + 1) by A34, A35, CARD_2: 41;

        then (A \/ {x}) in the Lines of ( G_ (k,X)) by A14, A39;

        then

        consider L be LINE of ( G_ (k,X)) such that

         A40: L = (A \/ {x});

        (k - 1) <= ((k - 1) + 1) by A29, NAT_1: 11;

        then ( Segm k1) c= ( Segm ( card AA)) by A34, NAT_1: 39;

        then

        consider B2 be set such that

         A41: B2 c= A and

         A42: ( card B2) = (k - 1) by CARD_FIL: 36;

        

         A43: B2 is finite by A3, A42, NAT_1: 21, XXREAL_0: 2;

        B2 c= X by A34, A41, XBOOLE_1: 1;

        then

         A44: (B2 \/ {x}) c= X by A38, XBOOLE_1: 8;

         not x in B2 by A37, A41, XBOOLE_0:def 5;

        then ( card (B2 \/ {x})) = ((k - 1) + 1) by A42, A43, CARD_2: 41;

        then (B2 \/ {x}) in the Points of ( G_ (k,X)) by A7, A44;

        then

        consider A1 be POINT of ( G_ (k,X)) such that

         A45: A1 = (B2 \/ {x});

        

         A46: {x} c= L by A40, XBOOLE_1: 7;

        

         A47: A c= L by A40, XBOOLE_1: 7;

        then B2 c= L by A41;

        then A1 c= L by A45, A46, XBOOLE_1: 8;

        then

         A48: A1 on L by A3, A6, Th10;

         {x} c= A1 by A45, XBOOLE_1: 7;

        then x in A1 by ZFMISC_1: 31;

        then

         A49: A <> A1 by A37, XBOOLE_0:def 5;

        consider U be Subset of the Points of ( G_ (k,X)) such that

         A50: U = {A, A1};

        

         A51: A on L by A3, A6, A47, Th10;

        

         A52: U is clique

        proof

          let B1,B2 be POINT of ( G_ (k,X));

          assume B1 in U & B2 in U;

          then B1 on L & B2 on L by A51, A48, A50, TARSKI:def 2;

          then {B1, B2} on L by INCSP_1: 1;

          hence thesis;

        end;

        A in U by A50, TARSKI:def 2;

        then

         A53: K c= U by A31, A33, ZFMISC_1: 31;

        A1 in U by A50, TARSKI:def 2;

        then U <> K by A31, A33, A49, TARSKI:def 1;

        hence contradiction by A12, A53, A52;

      end;

      ( succ 1) = (1 + 1);

      then

       A54: 2 c= ( card K) by A30, A28, ORDINAL1: 21;

      then

      consider R be set such that

       A55: R c= K and

       A56: ( card R) = 2 by CARD_FIL: 36;

      consider A1,B1 be object such that

       A57: A1 <> B1 and

       A58: R = {A1, B1} by A56, CARD_2: 60;

      

       A59: A1 in R by A58, TARSKI:def 2;

      then

       A60: A1 in the Points of ( G_ (k,X)) by A55, TARSKI:def 3;

      then

      consider A be POINT of ( G_ (k,X)) such that

       A61: A = A1;

      

       A62: B1 in R by A58, TARSKI:def 2;

      then

       A63: B1 in the Points of ( G_ (k,X)) by A55, TARSKI:def 3;

      then

      consider B be POINT of ( G_ (k,X)) such that

       A64: B = B1;

      consider L be LINE of ( G_ (k,X)) such that

       A65: {A, B} on L by A13, A55, A59, A62, A61, A64;

      L in the Lines of ( G_ (k,X));

      then

       A66: ex L1 be Subset of X st L1 = L & ( card L1) = (k + 1) by A14;

      then

       A67: L is finite;

      A on L by A65, INCSP_1: 1;

      then

       A68: A c= L by A3, A6, Th10;

      then

       A69: (A /\ B) c= L by XBOOLE_1: 108;

      then

       A70: (A /\ B) c= X by A66, XBOOLE_1: 1;

      B on L by A65, INCSP_1: 1;

      then

       A71: B c= L by A3, A6, Th10;

      then

       A72: (A \/ B) c= L by A68, XBOOLE_1: 8;

      then

       A73: ( card (A \/ B)) c= (k + 1) by A66, CARD_1: 11;

      

       A74: ex B2 be Subset of X st B2 = B & ( card B2) = k by A7, A63, A64;

      then

       A75: B is finite;

      

       A76: ex A2 be Subset of X st A2 = A & ( card A2) = k by A7, A60, A61;

      then

       A77: A is finite;

      

       A78: (k + 1) c= ( card (A \/ B)) by A57, A61, A64, A76, A74, Th1;

      then

       A79: ( card (A \/ B)) = (k + 1) by A73, XBOOLE_0:def 10;

      then

       A80: (A \/ B) = L by A68, A71, A66, A67, CARD_2: 102, XBOOLE_1: 8;

      

       A81: not (ex C be POINT of ( G_ (k,X)) st C in K & C on L & A <> C & B <> C) implies K is STAR

      proof

        

         A82: ( card L) <> ( card X)

        proof

          assume ( card L) = ( card X);

          then (k + 1) in (k + 1) by A4, A8, A66, ORDINAL1: 21;

          hence contradiction;

        end;

        ( card L) c= ( card X) by A4, A5, A66;

        then ( card L) in ( card X) by A82, CARD_1: 3;

        then (X \ L) <> {} by CARD_1: 68;

        then

        consider x be object such that

         A83: x in (X \ L) by XBOOLE_0:def 1;

        

         A84: ( not x in A) & not x in B by A68, A71, A83, XBOOLE_0:def 5;

        

         A85: (A /\ {x}) = {} & (B /\ {x}) = {}

        proof

          assume (A /\ {x}) <> {} or (B /\ {x}) <> {} ;

          then

          consider z1 be object such that

           A86: z1 in (A /\ {x}) or z1 in (B /\ {x}) by XBOOLE_0:def 1;

          z1 in A & z1 in {x} or z1 in B & z1 in {x} by A86, XBOOLE_0:def 4;

          hence contradiction by A84, TARSKI:def 1;

        end;

        

         A87: ( card A) = ((k - 1) + 1) & ( card (A \/ B)) = ((k - 1) + (2 * 1)) by A76, A73, A78, XBOOLE_0:def 10;

        then

         A88: ( card (A /\ B)) = (k - 1) by A29, A74, Th2;

        then ( card (A \ (A /\ B))) = (k - (k - 1)) by A76, A77, CARD_2: 44, XBOOLE_1: 17;

        then

        consider z1 be object such that

         A89: (A \ (A /\ B)) = {z1} by CARD_2: 42;

        ( card (B \ (A /\ B))) = (k - (k - 1)) by A74, A75, A88, CARD_2: 44, XBOOLE_1: 17;

        then

        consider z2 be object such that

         A90: (B \ (A /\ B)) = {z2} by CARD_2: 42;

        

         A91: B = ((A /\ B) \/ {z2}) by A90, XBOOLE_1: 17, XBOOLE_1: 45;

        

         A92: z2 in {z2} by TARSKI:def 1;

        

         A93: ( card (A \/ B)) = ((k - 1) + (2 * 1)) by A73, A78, XBOOLE_0:def 10;

        

         A94: not x in (A /\ B) by A69, A83, XBOOLE_0:def 5;

        ( card A) = ((k - 1) + 1) by A76;

        then ( card (A /\ B)) = (k - 1) by A29, A74, A93, Th2;

        then

         A95: ( card ((A /\ B) \/ {x})) = ((k - 1) + 1) by A68, A67, A94, CARD_2: 41;

         {x} c= X by A83, ZFMISC_1: 31;

        then

         A96: ((A /\ B) \/ {x}) c= X by A70, XBOOLE_1: 8;

        then ((A /\ B) \/ {x}) in the Points of ( G_ (k,X)) by A7, A95;

        then

        consider C be POINT of ( G_ (k,X)) such that

         A97: C = ((A /\ B) \/ {x});

        

         A98: (B \/ C) c= X by A74, A96, A97, XBOOLE_1: 8;

        

         A99: (A \/ C) c= X by A76, A96, A97, XBOOLE_1: 8;

        

         A100: (1 + 1) <= (k + 1) by A9, XREAL_1: 7;

        

         A101: (A /\ B) c= B by XBOOLE_1: 17;

        (B /\ C) = ((B /\ {x}) \/ (B /\ (B /\ A))) by A97, XBOOLE_1: 23;

        then (B /\ C) = ((B /\ {x}) \/ ((B /\ B) /\ A)) by XBOOLE_1: 16;

        then ( card (B /\ C)) = (k - 1) by A29, A74, A85, A87, Th2;

        then ( card (B \/ C)) = ((k - 1) + (2 * 1)) by A29, A74, A95, A97, Th2;

        then (B \/ C) in the Lines of ( G_ (k,X)) by A14, A98;

        then

        consider L2 be LINE of ( G_ (k,X)) such that

         A102: L2 = (B \/ C);

        (A /\ C) = ((A /\ {x}) \/ (A /\ (A /\ B))) by A97, XBOOLE_1: 23;

        then (A /\ C) = ((A /\ {x}) \/ ((A /\ A) /\ B)) by XBOOLE_1: 16;

        then ( card (A /\ C)) = (k - 1) by A29, A74, A85, A87, Th2;

        then ( card (A \/ C)) = ((k - 1) + (2 * 1)) by A29, A76, A95, A97, Th2;

        then (A \/ C) in the Lines of ( G_ (k,X)) by A14, A99;

        then

        consider L1 be LINE of ( G_ (k,X)) such that

         A103: L1 = (A \/ C);

        

         A104: {A, B, C} is clique

        proof

          let Z1,Z2 be POINT of ( G_ (k,X));

          assume that

           A105: Z1 in {A, B, C} and

           A106: Z2 in {A, B, C};

          

           A107: Z2 = A or Z2 = B or Z2 = C by A106, ENUMSET1:def 1;

          Z1 = A or Z1 = B or Z1 = C by A105, ENUMSET1:def 1;

          then Z1 c= (A \/ B) & Z2 c= (A \/ B) or Z1 c= (A \/ C) & Z2 c= (A \/ C) or Z1 c= (B \/ C) & Z2 c= (B \/ C) by A107, XBOOLE_1: 11;

          then Z1 on L & Z2 on L or Z1 on L1 & Z2 on L1 or Z1 on L2 & Z2 on L2 by A3, A6, A80, A103, A102, Th10;

          then {Z1, Z2} on L or {Z1, Z2} on L1 or {Z1, Z2} on L2 by INCSP_1: 1;

          hence thesis;

        end;

        

         A108: C <> A & C <> B by A84, A97, XBOOLE_1: 11, ZFMISC_1: 31;

        

         A109: 3 c= ( card K)

        proof

          assume not 3 c= ( card K);

          then ( card K) in 3 by ORDINAL1: 16;

          then ( card K) c= 2 by A2, ORDINAL1: 22;

          then ( card K) = 2 & K is finite by A54, XBOOLE_0:def 10;

          then

           A110: K = {A, B} by A55, A56, A58, A61, A64, CARD_2: 102;

          A in {A, B, C} & B in {A, B, C} by ENUMSET1:def 1;

          then

           A111: {A, B} c= {A, B, C} by ZFMISC_1: 32;

          C in {A, B, C} by ENUMSET1:def 1;

          then not {A, B, C} c= {A, B} by A108, TARSKI:def 2;

          hence contradiction by A12, A104, A110, A111;

        end;

        ( card {A, B}) <> ( card K)

        proof

          assume ( card {A, B}) = ( card K);

          then 3 in 3 by A2, A56, A58, A61, A64, A109, ORDINAL1: 22;

          hence contradiction;

        end;

        then ( card {A, B}) in ( card K) by A54, A56, A58, A61, A64, CARD_1: 3;

        then (K \ {A, B}) <> {} by CARD_1: 68;

        then

        consider E2 be object such that

         A112: E2 in (K \ {A, B}) by XBOOLE_0:def 1;

        

         A113: ( card A) = ((k - 1) + 1) by A76;

        then

         A114: ( card (A /\ B)) = ((k + 1) - 2) by A29, A74, A93, Th2;

        

         A115: ( card B) = ((k - 1) + 1) by A74;

        

         A116: (A /\ B) c= A by XBOOLE_1: 17;

        

         A117: not E2 in {A, B} by A112, XBOOLE_0:def 5;

        then

         A118: E2 <> A by TARSKI:def 2;

        E2 in the Points of ( G_ (k,X)) by A112;

        then

        consider E1 be Subset of X such that

         A119: E1 = E2 and

         A120: ( card E1) = k by A7;

        consider E be POINT of ( G_ (k,X)) such that

         A121: E = E1 by A112, A119;

        

         A122: A = ((A /\ B) \/ {z1}) by A89, XBOOLE_1: 17, XBOOLE_1: 45;

        

         A123: z1 in {z1} by TARSKI:def 1;

        then

         A124: not z1 in (A /\ B) by A89, XBOOLE_0:def 5;

        

         A125: ( card A) = ((k + 1) - 1) & (2 + 1) <= (k + 1) by A3, A76, XREAL_1: 7;

        consider S be set such that

         A126: S = { D where D be Subset of X : ( card D) = k & (A /\ B) c= D };

        

         A127: E2 in K by A112, XBOOLE_0:def 5;

        then

        consider K1 be LINE of ( G_ (k,X)) such that

         A128: {A, E} on K1 by A13, A55, A59, A61, A119, A121;

        consider K2 be LINE of ( G_ (k,X)) such that

         A129: {B, E} on K2 by A13, A55, A62, A64, A127, A119, A121;

        E on K2 by A129, INCSP_1: 1;

        then

         A130: E c= K2 by A3, A6, Th10;

        K2 in the Lines of ( G_ (k,X));

        then

         A131: ex M2 be Subset of X st K2 = M2 & ( card M2) = (k + 1) by A14;

        B on K2 by A129, INCSP_1: 1;

        then B c= K2 by A3, A6, Th10;

        then (B \/ E) c= K2 by A130, XBOOLE_1: 8;

        then

         A132: ( card (B \/ E)) c= (k + 1) by A131, CARD_1: 11;

        

         A133: E2 <> B by A117, TARSKI:def 2;

        then (k + 1) c= ( card (B \/ E)) by A74, A119, A120, A121, Th1;

        then ( card (B \/ E)) = ((k - 1) + (2 * 1)) by A132, XBOOLE_0:def 10;

        then

         A134: ( card (B /\ E)) = ((k + 1) - 2) by A29, A120, A121, A115, Th2;

        assume not (ex C be POINT of ( G_ (k,X)) st C in K & C on L & A <> C & B <> C);

        then

         A135: not E on L by A127, A118, A133, A119, A121;

        

         A136: not ( card ((A \/ B) \/ E)) = (k + 1)

        proof

          assume

           A137: ( card ((A \/ B) \/ E)) = (k + 1);

          then (A \/ B) c= ((A \/ B) \/ E) & ((A \/ B) \/ E) is finite by XBOOLE_1: 7;

          then

           A138: (A \/ B) = ((A \/ B) \/ E) by A79, A137, CARD_2: 102;

          E c= ((A \/ B) \/ E) by XBOOLE_1: 7;

          then E c= L by A72, A138;

          hence contradiction by A3, A6, A135, Th10;

        end;

        E on K1 by A128, INCSP_1: 1;

        then

         A139: E c= K1 by A3, A6, Th10;

        K1 in the Lines of ( G_ (k,X));

        then

         A140: ex M1 be Subset of X st K1 = M1 & ( card M1) = (k + 1) by A14;

        A on K1 by A128, INCSP_1: 1;

        then A c= K1 by A3, A6, Th10;

        then (A \/ E) c= K1 by A139, XBOOLE_1: 8;

        then

         A141: ( card (A \/ E)) c= (k + 1) by A140, CARD_1: 11;

        (k + 1) c= ( card (A \/ E)) by A76, A118, A119, A120, A121, Th1;

        then ( card (A \/ E)) = ((k - 1) + (2 * 1)) by A141, XBOOLE_0:def 10;

        then ( card (A /\ E)) = ((k + 1) - 2) by A29, A120, A121, A113, Th2;

        then ( card ((A /\ B) /\ E)) = ((k + 1) - 2) & ( card ((A \/ B) \/ E)) = ((k + 1) + 1) or ( card ((A /\ B) /\ E)) = ((k + 1) - 3) & ( card ((A \/ B) \/ E)) = (k + 1) by A74, A120, A121, A134, A125, A100, A114, Th7;

        then

         A142: (A /\ B) = ((A /\ B) /\ E) by A68, A67, A88, A136, CARD_2: 102, XBOOLE_1: 17;

        then

         A143: (A /\ B) c= E by XBOOLE_1: 17;

        E is finite by A120, A121;

        then ( card (E \ (A /\ B))) = (k - (k - 1)) by A88, A120, A121, A142, CARD_2: 44, XBOOLE_1: 17;

        then

        consider z4 be object such that

         A144: (E \ (A /\ B)) = {z4} by CARD_2: 42;

        

         A145: E = ((A /\ B) \/ {z4}) by A142, A144, XBOOLE_1: 17, XBOOLE_1: 45;

        

         A146: K c= S

        proof

          assume not K c= S;

          then

          consider D2 be object such that

           A147: D2 in K and

           A148: not D2 in S;

          D2 in the Points of ( G_ (k,X)) by A147;

          then

          consider D1 be Subset of X such that

           A149: D1 = D2 and

           A150: ( card D1) = k by A7;

          consider D be POINT of ( G_ (k,X)) such that

           A151: D = D1 by A147, A149;

          consider K11 be LINE of ( G_ (k,X)) such that

           A152: {A, D} on K11 by A13, A55, A59, A61, A147, A149, A151;

          D on K11 by A152, INCSP_1: 1;

          then

           A153: D c= K11 by A3, A6, Th10;

          K11 in the Lines of ( G_ (k,X));

          then

           A154: ex R11 be Subset of X st R11 = K11 & ( card R11) = (k + 1) by A14;

          

           A155: ( card D) = ((k - 1) + 1) by A150, A151;

          consider K13 be LINE of ( G_ (k,X)) such that

           A156: {E, D} on K13 by A13, A127, A119, A121, A147, A149, A151;

          consider K12 be LINE of ( G_ (k,X)) such that

           A157: {B, D} on K12 by A13, A55, A62, A64, A147, A149, A151;

          A on K11 by A152, INCSP_1: 1;

          then A c= K11 by A3, A6, Th10;

          then (A \/ D) c= K11 by A153, XBOOLE_1: 8;

          then

           A158: ( card (A \/ D)) c= (k + 1) by A154, CARD_1: 11;

          A <> D by A126, A116, A148, A149, A150, A151;

          then (k + 1) c= ( card (A \/ D)) by A76, A150, A151, Th1;

          then ( card (A \/ D)) = ((k - 1) + (2 * 1)) by A158, XBOOLE_0:def 10;

          then

           A159: ( card (A /\ D)) = (k - 1) by A29, A76, A155, Th2;

           not (A /\ B) c= D by A126, A148, A149, A150, A151;

          then ex y be object st y in (A /\ B) & not y in D;

          then (A /\ B) <> ((A /\ B) /\ D) by XBOOLE_0:def 4;

          then

           A160: ( card ((A /\ B) /\ D)) <> ( card (A /\ B)) by A77, CARD_2: 102, XBOOLE_1: 17;

          D on K13 by A156, INCSP_1: 1;

          then

           A161: D c= K13 by A3, A6, Th10;

          K13 in the Lines of ( G_ (k,X));

          then

           A162: ex R13 be Subset of X st R13 = K13 & ( card R13) = (k + 1) by A14;

          D on K12 by A157, INCSP_1: 1;

          then

           A163: D c= K12 by A3, A6, Th10;

          K12 in the Lines of ( G_ (k,X));

          then

           A164: ex R12 be Subset of X st R12 = K12 & ( card R12) = (k + 1) by A14;

          B on K12 by A157, INCSP_1: 1;

          then B c= K12 by A3, A6, Th10;

          then (B \/ D) c= K12 by A163, XBOOLE_1: 8;

          then

           A165: ( card (B \/ D)) c= (k + 1) by A164, CARD_1: 11;

          B <> D by A126, A101, A148, A149, A150, A151;

          then (k + 1) c= ( card (B \/ D)) by A74, A150, A151, Th1;

          then ( card (B \/ D)) = ((k - 1) + (2 * 1)) by A165, XBOOLE_0:def 10;

          then

           A166: ( card (B /\ D)) = (k - 1) by A29, A74, A155, Th2;

          E on K13 by A156, INCSP_1: 1;

          then E c= K13 by A3, A6, Th10;

          then (E \/ D) c= K13 by A161, XBOOLE_1: 8;

          then

           A167: ( card (E \/ D)) c= (k + 1) by A162, CARD_1: 11;

          E <> D by A126, A143, A148, A149, A150, A151;

          then (k + 1) c= ( card (E \/ D)) by A120, A121, A150, A151, Th1;

          then ( card (E \/ D)) = ((k - 1) + (2 * 1)) by A167, XBOOLE_0:def 10;

          then

           A168: ( card (E /\ D)) = (k - 1) by A29, A120, A121, A155, Th2;

          

           A169: z1 in D & z2 in D & z4 in D

          proof

            assume not z1 in D or not z2 in D or not z4 in D;

            then (A /\ D) = (((A /\ B) \/ {z1}) /\ D) & {z1} misses D or (B /\ D) = (((A /\ B) \/ {z2}) /\ D) & {z2} misses D or (E /\ D) = (((A /\ B) \/ {z4}) /\ D) & {z4} misses D by A89, A90, A142, A144, XBOOLE_1: 17, XBOOLE_1: 45, ZFMISC_1: 50;

            then (A /\ D) = (((A /\ B) /\ D) \/ ( {z1} /\ D)) & ( {z1} /\ D) = {} or (B /\ D) = (((A /\ B) /\ D) \/ ( {z2} /\ D)) & ( {z2} /\ D) = {} or (E /\ D) = (((A /\ B) /\ D) \/ ( {z4} /\ D)) & ( {z4} /\ D) = {} by XBOOLE_0:def 7, XBOOLE_1: 23;

            hence contradiction by A29, A74, A87, A159, A166, A168, A160, Th2;

          end;

          then {z1, z2} c= D & {z4} c= D by ZFMISC_1: 31, ZFMISC_1: 32;

          then ( {z1, z2} \/ {z4}) c= D by XBOOLE_1: 8;

          then ((A /\ B) /\ D) c= D & {z1, z2, z4} c= D by ENUMSET1: 3, XBOOLE_1: 17;

          then

           A170: (((A /\ B) /\ D) \/ {z1, z2, z4}) c= D by XBOOLE_1: 8;

          

           A171: z4 in (E \ (A /\ B)) & ((A /\ B) /\ D) c= (A /\ B) by A144, TARSKI:def 1, XBOOLE_1: 17;

          

           A172: {z1, z2, z4} misses ((A /\ B) /\ D)

          proof

            assume not {z1, z2, z4} misses ((A /\ B) /\ D);

            then ( {z1, z2, z4} /\ ((A /\ B) /\ D)) <> {} by XBOOLE_0:def 7;

            then

            consider m be object such that

             A173: m in ( {z1, z2, z4} /\ ((A /\ B) /\ D)) by XBOOLE_0:def 1;

            m in {z1, z2, z4} by A173, XBOOLE_0:def 4;

            then

             A174: m = z1 or m = z2 or m = z4 by ENUMSET1:def 1;

            m in ((A /\ B) /\ D) by A173, XBOOLE_0:def 4;

            hence contradiction by A89, A90, A123, A92, A171, A174, XBOOLE_0:def 5;

          end;

          reconsider r = ( card ((A /\ B) /\ D)) as Nat by A77;

          

           A175: not z1 in ((A /\ B) /\ D) by A124, XBOOLE_0:def 4;

          (A /\ D) = (((A /\ B) \/ {z1}) /\ D) by A89, XBOOLE_1: 17, XBOOLE_1: 45;

          then (A /\ D) = (((A /\ B) /\ D) \/ ( {z1} /\ D)) by XBOOLE_1: 23;

          then (A /\ D) = (((A /\ B) /\ D) \/ {z1}) by A169, ZFMISC_1: 46;

          then

           A176: ( card (A /\ D)) = (r + 1) by A77, A175, CARD_2: 41;

          ( card {z1, z2, z4}) = 3 by A57, A61, A64, A122, A91, A118, A133, A119, A121, A145, CARD_2: 58;

          then ( card (((A /\ B) /\ D) \/ {z1, z2, z4})) = ((k - 2) + 3) by A77, A159, A176, A172, CARD_2: 40;

          then (k + 1) c= k by A150, A151, A170, CARD_1: 11;

          then k in k by A10, ORDINAL1: 21;

          hence contradiction;

        end;

        S c= the Points of ( G_ (k,X))

        proof

          let Z be object;

          assume Z in S;

          then ex Z1 be Subset of X st Z = Z1 & ( card Z1) = k & (A /\ B) c= Z1 by A126;

          hence thesis by A7;

        end;

        then

        consider S1 be Subset of the Points of ( G_ (k,X)) such that

         A177: S1 = S;

        

         A178: S1 is STAR by A70, A126, A88, A177;

        then S1 is maximal_clique by A3, A4, Th14;

        then S1 is clique;

        hence thesis by A12, A146, A177, A178;

      end;

      reconsider k2 = (k - 2) as Element of NAT by A3, NAT_1: 21;

      

       A179: ( succ ( Segm k2)) = ( Segm (k2 + 1)) by NAT_1: 38;

      (ex C be POINT of ( G_ (k,X)) st C in K & C on L & A <> C & B <> C) implies K is TOP

      proof

        

         A180: (1 + 1) <= (k + 1) by A9, XREAL_1: 7;

        

         A181: ( card B) = ((k - 1) + 1) by A74;

        

         A182: ( card A) = ((k - 1) + 1) by A76;

        assume ex C be POINT of ( G_ (k,X)) st C in K & C on L & A <> C & B <> C;

        then

        consider C be POINT of ( G_ (k,X)) such that

         A183: C in K and

         A184: C on L and

         A185: A <> C and

         A186: B <> C;

        

         A187: C c= L by A3, A6, A184, Th10;

        then (A \/ C) c= L by A68, XBOOLE_1: 8;

        then

         A188: ( card (A \/ C)) c= (k + 1) by A66, CARD_1: 11;

        (B \/ C) c= L by A71, A187, XBOOLE_1: 8;

        then

         A189: ( card (B \/ C)) c= (k + 1) by A66, CARD_1: 11;

        C in the Points of ( G_ (k,X));

        then

         A190: ex C2 be Subset of X st C2 = C & ( card C2) = k by A7;

        then (k + 1) c= ( card (B \/ C)) by A74, A186, Th1;

        then ( card (B \/ C)) = ((k - 1) + (2 * 1)) by A189, XBOOLE_0:def 10;

        then

         A191: ( card (B /\ C)) = ((k + 1) - 2) by A29, A190, A181, Th2;

        (k + 1) c= ( card (A \/ C)) by A76, A185, A190, Th1;

        then ( card (A \/ C)) = ((k - 1) + (2 * 1)) by A188, XBOOLE_0:def 10;

        then

         A192: ( card (A /\ C)) = ((k + 1) - 2) by A29, A190, A182, Th2;

        

         A193: ( card (A \/ B)) = ((k - 1) + (2 * 1)) by A73, A78, XBOOLE_0:def 10;

        then

         A194: (A \/ B) = L by A68, A71, A66, A67, CARD_2: 102, XBOOLE_1: 8;

        

         A195: (A \/ B) c= ((A \/ B) \/ C) by XBOOLE_1: 7;

        ((A \/ B) \/ C) c= L by A72, A187, XBOOLE_1: 8;

        then

         A196: ( card ((A \/ B) \/ C)) = (k + 1) by A193, A194, A195, XBOOLE_0:def 10;

        

         A197: ( card A) = ((k + 1) - 1) & (2 + 1) <= (k + 1) by A3, A76, XREAL_1: 7;

        consider T be set such that

         A198: T = { D where D be Subset of X : ( card D) = k & D c= L };

        ( card (A /\ B)) = (k - 1) by A29, A74, A193, A182, Th2;

        then

         A199: ( card ((A /\ B) /\ C)) = ((k + 1) - 3) & ( card ((A \/ B) \/ C)) = (k + 1) or ( card ((A /\ B) /\ C)) = ((k + 1) - 2) & ( card ((A \/ B) \/ C)) = ((k + 1) + 1) by A74, A190, A192, A197, A191, A180, Th7;

        

         A200: K c= T

        proof

          let D2 be object;

          assume that

           A201: D2 in K and

           A202: not D2 in T;

          D2 in the Points of ( G_ (k,X)) by A201;

          then

          consider D1 be Subset of X such that

           A203: D1 = D2 and

           A204: ( card D1) = k by A7;

          consider D be POINT of ( G_ (k,X)) such that

           A205: D = D1 by A201, A203;

           not D c= L by A198, A202, A203, A204, A205;

          then

          consider x be object such that

           A206: x in D and

           A207: not x in L;

          

           A208: ( card {x}) = 1 by CARD_1: 30;

          

           A209: D is finite by A204, A205;

          

           A210: ( card D) = ((k - 1) + 1) by A204, A205;

           {x} c= D by A206, ZFMISC_1: 31;

          then

           A211: ( card (D \ {x})) = (k - 1) by A204, A205, A209, A208, CARD_2: 44;

          consider L13 be LINE of ( G_ (k,X)) such that

           A212: {C, D} on L13 by A13, A183, A201, A203, A205;

          D on L13 by A212, INCSP_1: 1;

          then

           A213: D c= L13 by A3, A6, Th10;

          L13 in the Lines of ( G_ (k,X));

          then

           A214: ex L23 be Subset of X st L23 = L13 & ( card L23) = (k + 1) by A14;

          C on L13 by A212, INCSP_1: 1;

          then C c= L13 by A3, A6, Th10;

          then (C \/ D) c= L13 by A213, XBOOLE_1: 8;

          then

           A215: ( card (C \/ D)) c= (k + 1) by A214, CARD_1: 11;

          

           A216: not x in C by A187, A207;

          

           A217: (C /\ D) c= (D \ {x})

          proof

            let z be object;

            assume

             A218: z in (C /\ D);

            then z <> x by A216, XBOOLE_0:def 4;

            then

             A219: not z in {x} by TARSKI:def 1;

            z in D by A218, XBOOLE_0:def 4;

            hence thesis by A219, XBOOLE_0:def 5;

          end;

          C <> D by A187, A198, A202, A203, A204, A205;

          then (k + 1) c= ( card (C \/ D)) by A190, A204, A205, Th1;

          then ( card (C \/ D)) = ((k - 1) + (2 * 1)) by A215, XBOOLE_0:def 10;

          then ( card (C /\ D)) = (k - 1) by A29, A190, A210, Th2;

          then

           A220: (C /\ D) = (D \ {x}) by A209, A211, A217, CARD_2: 102;

          consider L12 be LINE of ( G_ (k,X)) such that

           A221: {B, D} on L12 by A13, A55, A62, A64, A201, A203, A205;

          consider L11 be LINE of ( G_ (k,X)) such that

           A222: {A, D} on L11 by A13, A55, A59, A61, A201, A203, A205;

          D on L11 by A222, INCSP_1: 1;

          then

           A223: D c= L11 by A3, A6, Th10;

          L11 in the Lines of ( G_ (k,X));

          then

           A224: ex L21 be Subset of X st L21 = L11 & ( card L21) = (k + 1) by A14;

          A on L11 by A222, INCSP_1: 1;

          then A c= L11 by A3, A6, Th10;

          then (A \/ D) c= L11 by A223, XBOOLE_1: 8;

          then

           A225: ( card (A \/ D)) c= (k + 1) by A224, CARD_1: 11;

          

           A226: not x in A by A68, A207;

          

           A227: (A /\ D) c= (D \ {x})

          proof

            let z be object;

            assume

             A228: z in (A /\ D);

            then z <> x by A226, XBOOLE_0:def 4;

            then

             A229: not z in {x} by TARSKI:def 1;

            z in D by A228, XBOOLE_0:def 4;

            hence thesis by A229, XBOOLE_0:def 5;

          end;

          A <> D by A68, A198, A202, A203, A204, A205;

          then (k + 1) c= ( card (A \/ D)) by A76, A204, A205, Th1;

          then

           A230: ( card (A \/ D)) = ((k - 1) + (2 * 1)) by A225, XBOOLE_0:def 10;

          then ( card (A /\ D)) = (k - 1) by A29, A76, A210, Th2;

          then

           A231: (A /\ D) = (D \ {x}) by A209, A211, A227, CARD_2: 102;

          D on L12 by A221, INCSP_1: 1;

          then

           A232: D c= L12 by A3, A6, Th10;

          L12 in the Lines of ( G_ (k,X));

          then

           A233: ex L22 be Subset of X st L22 = L12 & ( card L22) = (k + 1) by A14;

          B on L12 by A221, INCSP_1: 1;

          then B c= L12 by A3, A6, Th10;

          then (B \/ D) c= L12 by A232, XBOOLE_1: 8;

          then

           A234: ( card (B \/ D)) c= (k + 1) by A233, CARD_1: 11;

          

           A235: not x in B by A71, A207;

          

           A236: (B /\ D) c= (D \ {x})

          proof

            let z be object;

            assume

             A237: z in (B /\ D);

            then z <> x by A235, XBOOLE_0:def 4;

            then

             A238: not z in {x} by TARSKI:def 1;

            z in D by A237, XBOOLE_0:def 4;

            hence thesis by A238, XBOOLE_0:def 5;

          end;

          B <> D by A71, A198, A202, A203, A204, A205;

          then (k + 1) c= ( card (B \/ D)) by A74, A204, A205, Th1;

          then ( card (B \/ D)) = ((k - 1) + (2 * 1)) by A234, XBOOLE_0:def 10;

          then ( card (B /\ D)) = (k - 1) by A29, A74, A210, Th2;

          then (B /\ D) = (D \ {x}) by A209, A211, A236, CARD_2: 102;

          then (A /\ D) = ((A /\ D) /\ (B /\ D)) by A231;

          then (A /\ D) = ((A /\ (D /\ B)) /\ D) by XBOOLE_1: 16;

          then (A /\ D) = (((A /\ B) /\ D) /\ D) by XBOOLE_1: 16;

          then (A /\ D) = ((A /\ B) /\ (D /\ D)) by XBOOLE_1: 16;

          then (A /\ D) = (((A /\ B) /\ D) /\ (C /\ D)) by A231, A220;

          then (A /\ D) = (((A /\ B) /\ (D /\ C)) /\ D) by XBOOLE_1: 16;

          then (A /\ D) = ((((A /\ B) /\ C) /\ D) /\ D) by XBOOLE_1: 16;

          then (A /\ D) = (((A /\ B) /\ C) /\ (D /\ D)) by XBOOLE_1: 16;

          then ( card (((A /\ B) /\ C) /\ D)) = (k - 1) by A29, A76, A210, A230, Th2;

          then (k - 1) c= k2 by A196, A199, CARD_1: 11, XBOOLE_1: 17;

          then (k - 1) in (k - 1) by A179, ORDINAL1: 22;

          hence contradiction;

        end;

        T c= the Points of ( G_ (k,X))

        proof

          let e be object;

          assume e in T;

          then ex E be Subset of X st e = E & ( card E) = k & E c= L by A198;

          hence thesis by A7;

        end;

        then

        consider T1 be Subset of the Points of ( G_ (k,X)) such that

         A239: T1 = T;

        

         A240: T1 is TOP by A66, A198, A239;

        then T1 is maximal_clique by A3, A4, Th14;

        then T1 is clique;

        hence thesis by A12, A200, A239, A240;

      end;

      hence thesis by A81;

    end;

    begin

    definition

      let S1,S2 be IncProjStr;

      struct IncProjMap over S1,S2 (# the point-map -> Function of the Points of S1, the Points of S2,

the line-map -> Function of the Lines of S1, the Lines of S2 #)

       attr strict strict;

    end

    definition

      let S1,S2 be IncProjStr;

      let F be IncProjMap over S1, S2;

      let a be POINT of S1;

      :: COMBGRAS:def6

      func F . a -> POINT of S2 equals (the point-map of F . a);

      coherence ;

    end

    definition

      let S1,S2 be IncProjStr;

      let F be IncProjMap over S1, S2;

      let L be LINE of S1;

      :: COMBGRAS:def7

      func F . L -> LINE of S2 equals (the line-map of F . L);

      coherence ;

    end

    theorem :: COMBGRAS:16

    

     Th16: for S1,S2 be IncProjStr holds for F1,F2 be IncProjMap over S1, S2 st (for A be POINT of S1 holds (F1 . A) = (F2 . A)) & (for L be LINE of S1 holds (F1 . L) = (F2 . L)) holds the IncProjMap of F1 = the IncProjMap of F2

    proof

      let S1,S2 be IncProjStr;

      let F1,F2 be IncProjMap over S1, S2;

      assume that

       A1: for A be POINT of S1 holds (F1 . A) = (F2 . A) and

       A2: for L be LINE of S1 holds (F1 . L) = (F2 . L);

      for a be object holds (a in the Points of S1 implies (the point-map of F1 . a) = (the point-map of F2 . a))

      proof

        let a be object;

        assume a in the Points of S1;

        then

        consider A be POINT of S1 such that

         A3: A = a;

        (F1 . A) = (F2 . A) by A1;

        hence thesis by A3;

      end;

      then

       A4: the point-map of F1 = the point-map of F2 by FUNCT_2: 12;

      for l be object holds (l in the Lines of S1 implies (the line-map of F1 . l) = (the line-map of F2 . l))

      proof

        let l be object;

        assume l in the Lines of S1;

        then

        consider L be LINE of S1 such that

         A5: L = l;

        (F1 . L) = (F2 . L) by A2;

        hence thesis by A5;

      end;

      hence thesis by A4, FUNCT_2: 12;

    end;

    definition

      let S1,S2 be IncProjStr;

      let F be IncProjMap over S1, S2;

      :: COMBGRAS:def8

      attr F is incidence_preserving means for A1 be POINT of S1 holds for L1 be LINE of S1 holds (A1 on L1 iff (F . A1) on (F . L1));

    end

    theorem :: COMBGRAS:17

    for S1,S2 be IncProjStr holds for F1,F2 be IncProjMap over S1, S2 st the IncProjMap of F1 = the IncProjMap of F2 holds F1 is incidence_preserving implies F2 is incidence_preserving

    proof

      let S1,S2 be IncProjStr;

      let F1,F2 be IncProjMap over S1, S2;

      assume that

       A1: the IncProjMap of F1 = the IncProjMap of F2 and

       A2: F1 is incidence_preserving;

      let A1 be POINT of S1;

      let L1 be LINE of S1;

      (F2 . A1) = (F1 . A1) & (F2 . L1) = (F1 . L1) by A1;

      hence thesis by A2;

    end;

    definition

      let S be IncProjStr;

      let F be IncProjMap over S, S;

      :: COMBGRAS:def9

      attr F is automorphism means the line-map of F is bijective & the point-map of F is bijective & F is incidence_preserving;

    end

    definition

      let S1,S2 be IncProjStr;

      let F be IncProjMap over S1, S2;

      let K be Subset of the Points of S1;

      :: COMBGRAS:def10

      func F .: K -> Subset of the Points of S2 equals (the point-map of F .: K);

      coherence

      proof

        (the point-map of F .: K) c= the Points of S2

        proof

          let b be object;

          assume b in (the point-map of F .: K);

          then ex a be object st a in ( dom the point-map of F) & a in K & b = (the point-map of F . a) by FUNCT_1:def 6;

          hence thesis by FUNCT_2: 5;

        end;

        hence thesis;

      end;

    end

    definition

      let S1,S2 be IncProjStr;

      let F be IncProjMap over S1, S2;

      let K be Subset of the Points of S2;

      :: COMBGRAS:def11

      func F " K -> Subset of the Points of S1 equals (the point-map of F " K);

      coherence

      proof

        (the point-map of F " K) c= the Points of S1

        proof

          let b be object;

          assume b in (the point-map of F " K);

          then b in ( dom the point-map of F) by FUNCT_1:def 7;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let X be set;

      let A be finite set;

      :: COMBGRAS:def12

      func ^^ (A,X) -> Subset of ( bool X) equals { B where B be Subset of X : ( card B) = (( card A) + 1) & A c= B };

      coherence

      proof

        set Y = { B where B be Subset of X : ( card B) = (( card A) + 1) & A c= B };

        Y c= ( bool X)

        proof

          let x be object;

          assume x in Y;

          then ex B1 be Subset of X st x = B1 & ( card B1) = (( card A) + 1) & A c= B1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let k be Nat;

      let X be non empty set;

      let A be finite set;

      :: COMBGRAS:def13

      func ^^ (A,X,k) -> Subset of the Points of ( G_ (k,X)) equals

      : Def13: ( ^^ (A,X));

      coherence

      proof

        

         A3: the Points of ( G_ (k,X)) = { B where B be Subset of X : ( card B) = k } by A1, Def1;

        ( ^^ (A,X)) c= the Points of ( G_ (k,X))

        proof

          let x be object;

          assume x in ( ^^ (A,X));

          then ex B1 be Subset of X st x = B1 & ( card B1) = (( card A) + 1) & A c= B1;

          hence thesis by A2, A3;

        end;

        hence thesis;

      end;

    end

    theorem :: COMBGRAS:18

    

     Th18: for S1,S2 be IncProjStr holds for F be IncProjMap over S1, S2 holds for K be Subset of the Points of S1 holds (F .: K) = { B where B be POINT of S2 : ex A be POINT of S1 st (A in K & (F . A) = B) }

    proof

      let S1,S2 be IncProjStr;

      let F be IncProjMap over S1, S2;

      let K be Subset of the Points of S1;

      set Image = { B where B be POINT of S2 : ex A be POINT of S1 st (A in K & (F . A) = B) };

      

       A1: (F .: K) c= Image

      proof

        let b be object;

        assume b in (F .: K);

        then

        consider a be object such that

         A2: a in ( dom the point-map of F) and

         A3: a in K and

         A4: b = (the point-map of F . a) by FUNCT_1:def 6;

        consider A be POINT of S1 such that

         A5: a = A by A2;

        b in the Points of S2 by A2, A4, FUNCT_2: 5;

        then

        consider B1 be POINT of S2 such that

         A6: b = B1;

        (F . A) = B1 by A4, A5, A6;

        hence thesis by A3, A4, A5;

      end;

      Image c= (F .: K)

      proof

        let b be object;

        assume b in Image;

        then

         A7: ex B be POINT of S2 st B = b & ex A be POINT of S1 st A in K & (F . A) = B;

        the Points of S1 = ( dom the point-map of F) by FUNCT_2:def 1;

        hence thesis by A7, FUNCT_1:def 6;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: COMBGRAS:19

    for S1,S2 be IncProjStr holds for F be IncProjMap over S1, S2 holds for K be Subset of the Points of S2 holds (F " K) = { A where A be POINT of S1 : ex B be POINT of S2 st (B in K & (F . A) = B) }

    proof

      let S1,S2 be IncProjStr;

      let F be IncProjMap over S1, S2;

      let K be Subset of the Points of S2;

      set Image = { A where A be POINT of S1 : ex B be POINT of S2 st (B in K & (F . A) = B) };

      

       A1: (F " K) c= Image

      proof

        let a be object;

        assume

         A2: a in (F " K);

        then

        consider A be POINT of S1 such that

         A3: a = A;

        

         A4: (the point-map of F . a) in K by A2, FUNCT_1:def 7;

        then

        consider B1 be POINT of S2 such that

         A5: (the point-map of F . a) = B1;

        (F . A) = B1 by A3, A5;

        hence thesis by A4, A3;

      end;

      Image c= (F " K)

      proof

        let a be object;

        assume a in Image;

        then

         A6: ex A be POINT of S1 st A = a & ex B be POINT of S2 st B in K & (F . A) = B;

        the Points of S1 = ( dom the point-map of F) by FUNCT_2:def 1;

        hence thesis by A6, FUNCT_1:def 7;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: COMBGRAS:20

    

     Th20: for S be IncProjStr holds for F be IncProjMap over S, S holds for K be Subset of the Points of S holds F is incidence_preserving & K is clique implies (F .: K) is clique

    proof

      let S be IncProjStr;

      let F be IncProjMap over S, S;

      let K be Subset of the Points of S;

      assume that

       A1: F is incidence_preserving and

       A2: K is clique;

      let B1,B2 be POINT of S;

      assume that

       A3: B1 in (F .: K) and

       A4: B2 in (F .: K);

      

       A5: (F .: K) = { B where B be POINT of S : ex A be POINT of S st (A in K & (F . A) = B) } by Th18;

      then

      consider B11 be POINT of S such that

       A6: B1 = B11 and

       A7: ex A be POINT of S st A in K & (F . A) = B11 by A3;

      consider B12 be POINT of S such that

       A8: B2 = B12 and

       A9: ex A be POINT of S st A in K & (F . A) = B12 by A5, A4;

      consider A12 be POINT of S such that

       A10: A12 in K and

       A11: (F . A12) = B12 by A9;

      consider A11 be POINT of S such that

       A12: A11 in K and

       A13: (F . A11) = B11 by A7;

      consider L1 be LINE of S such that

       A14: {A11, A12} on L1 by A2, A12, A10;

      A12 on L1 by A14, INCSP_1: 1;

      then

       A15: (F . A12) on (F . L1) by A1;

      A11 on L1 by A14, INCSP_1: 1;

      then (F . A11) on (F . L1) by A1;

      then {B1, B2} on (F . L1) by A6, A8, A13, A11, A15, INCSP_1: 1;

      hence thesis;

    end;

    theorem :: COMBGRAS:21

    

     Th21: for S be IncProjStr holds for F be IncProjMap over S, S holds for K be Subset of the Points of S holds F is incidence_preserving & the line-map of F is onto & K is clique implies (F " K) is clique

    proof

      let S be IncProjStr;

      let F be IncProjMap over S, S;

      let K be Subset of the Points of S;

      assume that

       A1: F is incidence_preserving and

       A2: the line-map of F is onto and

       A3: K is clique;

      let A1,A2 be POINT of S;

      assume A1 in (F " K) & A2 in (F " K);

      then (F . A1) in K & (F . A2) in K by FUNCT_1:def 7;

      then

      consider L2 be LINE of S such that

       A4: {(F . A1), (F . A2)} on L2 by A3;

      the Lines of S = ( rng the line-map of F) by A2, FUNCT_2:def 3;

      then

      consider l1 be object such that

       A5: l1 in ( dom the line-map of F) and

       A6: L2 = (the line-map of F . l1) by FUNCT_1:def 3;

      consider L1 be LINE of S such that

       A7: L1 = l1 by A5;

      

       A8: L2 = (F . L1) by A6, A7;

      (F . A2) on L2 by A4, INCSP_1: 1;

      then

       A9: A2 on L1 by A1, A8;

      (F . A1) on L2 by A4, INCSP_1: 1;

      then A1 on L1 by A1, A8;

      then {A1, A2} on L1 by A9, INCSP_1: 1;

      hence thesis;

    end;

    theorem :: COMBGRAS:22

    

     Th22: for S be IncProjStr holds for F be IncProjMap over S, S holds for K be Subset of the Points of S holds F is automorphism & K is maximal_clique implies (F .: K) is maximal_clique & (F " K) is maximal_clique

    proof

      let S be IncProjStr;

      let F be IncProjMap over S, S;

      let K be Subset of the Points of S;

      assume that

       A1: F is automorphism and

       A2: K is maximal_clique;

      

       A3: F is incidence_preserving by A1;

      the point-map of F is bijective by A1;

      then

       A4: the Points of S = ( rng the point-map of F) by FUNCT_2:def 3;

      

       A5: the Points of S = ( dom the point-map of F) by FUNCT_2: 52;

      

       A6: for U be Subset of the Points of S st U is clique & (F " K) c= U holds U = (F " K)

      proof

        let U be Subset of the Points of S such that

         A7: U is clique and

         A8: (F " K) c= U;

        (F .: (F " K)) c= (F .: U) by A8, RELAT_1: 123;

        then

         A9: K c= (F .: U) by A4, FUNCT_1: 77;

        

         A10: U c= (F " (F .: U)) by A5, FUNCT_1: 76;

        (F .: U) is clique by A3, A7, Th20;

        then U c= (F " K) by A2, A9, A10;

        hence thesis by A8, XBOOLE_0:def 10;

      end;

      

       A11: the line-map of F is bijective by A1;

      

       A12: for U be Subset of the Points of S st U is clique & (F .: K) c= U holds U = (F .: K)

      proof

        

         A13: K c= (F " (F .: K)) by A5, FUNCT_1: 76;

        let U be Subset of the Points of S such that

         A14: U is clique and

         A15: (F .: K) c= U;

        (F " (F .: K)) c= (F " U) by A15, RELAT_1: 143;

        then

         A16: K c= (F " U) by A13;

        (F " U) is clique by A11, A3, A14, Th21;

        then (F .: (F " U)) c= (F .: K) by A2, A16;

        then U c= (F .: K) by A4, FUNCT_1: 77;

        hence thesis by A15, XBOOLE_0:def 10;

      end;

      

       A17: K is clique by A2;

      then

       A18: (F .: K) is clique by A3, Th20;

      (F " K) is clique by A11, A17, A3, Th21;

      hence thesis by A18, A12, A6;

    end;

    theorem :: COMBGRAS:23

    

     Th23: for k be Element of NAT holds for X be non empty set st 2 <= k & (k + 2) c= ( card X) holds for F be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) st F is automorphism holds for K be Subset of the Points of ( G_ (k,X)) holds K is STAR implies (F .: K) is STAR & (F " K) is STAR

    proof

      let k be Element of NAT ;

      let X be non empty set such that

       A1: 2 <= k and

       A2: (k + 2) c= ( card X);

      let F be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) such that

       A3: F is automorphism;

      

       A4: (k - 1) is Element of NAT by A1, NAT_1: 21, XXREAL_0: 2;

      then

      reconsider k1 = (k - 1) as Nat;

      

       A5: ( succ ( Segm k1)) = ( Segm (k1 + 1)) by NAT_1: 38;

      (2 - 1) <= (k - 1) by A1, XREAL_1: 9;

      then

       A6: ( Segm 1) c= ( Segm k1) by NAT_1: 39;

      

       A7: 1 <= k by A1, XXREAL_0: 2;

      then

       A8: ( Segm 1) c= ( Segm k) by NAT_1: 39;

      let K be Subset of the Points of ( G_ (k,X));

      assume

       A9: K is STAR;

      then

       A10: K is maximal_clique by A1, A2, Th14;

      then

       A11: K is clique;

      (k + 1) <= (k + 2) by XREAL_1: 7;

      then ( Segm (k + 1)) c= ( Segm (k + 2)) by NAT_1: 39;

      then

       A12: (k + 1) c= ( card X) by A2;

      then

       A13: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A1, Def1;

      

       A14: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, A12, Def1;

      

       A15: (k + 0 ) <= (k + 1) by XREAL_1: 7;

      then 1 <= (k + 1) by A7, XXREAL_0: 2;

      then

       A16: ( Segm 1) c= ( Segm (k + 1)) by NAT_1: 39;

      

       A17: not (F " K) is TOP

      proof

        assume (F " K) is TOP;

        then

        consider B be Subset of X such that

         A18: ( card B) = (k + 1) & (F " K) = { A where A be Subset of X : ( card A) = k & A c= B };

        consider X1 be set such that

         A19: X1 c= B & ( card X1) = 1 by A16, A18, CARD_FIL: 36;

        

         A20: B is finite by A18;

        then

         A21: ( card (B \ X1)) = ((k + 1) - 1) by A18, A19, CARD_2: 44;

        then

        consider X2 be set such that

         A22: X2 c= (B \ X1) and

         A23: ( card X2) = 1 by A8, CARD_FIL: 36;

        consider m be Nat such that

         A24: m = (k - 1) by A4;

        

         A25: ( card (B \ X2)) = ((k + 1) - 1) by A18, A20, A22, A23, CARD_2: 44, XBOOLE_1: 106;

        then (B \ X2) in the Points of ( G_ (k,X)) by A13;

        then

        consider B2 be POINT of ( G_ (k,X)) such that

         A26: (B \ X2) = B2;

        ( card ((B \ X1) \ X2)) = (k - 1) by A20, A21, A22, A23, CARD_2: 44;

        then

        consider X3 be set such that

         A27: X3 c= ((B \ X1) \ X2) and

         A28: ( card X3) = 1 by A6, CARD_FIL: 36;

        

         A29: X3 c= (B \ (X2 \/ X1)) by A27, XBOOLE_1: 41;

        then

         A30: ( card (B \ X3)) = ((k + 1) - 1) by A18, A20, A28, CARD_2: 44, XBOOLE_1: 106;

        then (B \ X3) in the Points of ( G_ (k,X)) by A13;

        then

        consider B3 be POINT of ( G_ (k,X)) such that

         A31: (B \ X3) = B3;

        B in the Lines of ( G_ (k,X)) by A14, A18;

        then

        consider L2 be LINE of ( G_ (k,X)) such that

         A32: B = L2;

        (B \ X1) in the Points of ( G_ (k,X)) by A13, A21;

        then

        consider B1 be POINT of ( G_ (k,X)) such that

         A33: (B \ X1) = B1;

        consider S be Subset of X such that

         A34: ( card S) = (k - 1) and

         A35: K = { A where A be Subset of X : ( card A) = k & S c= A } by A9;

        consider A1 be POINT of ( G_ (k,X)) such that

         A36: A1 = (F . B1);

        

         A37: X3 c= ((B \ X2) \ X1) by A29, XBOOLE_1: 41;

        

         A38: (B \ X1) <> (B \ X2) & (B \ X2) <> (B \ X3) & (B \ X1) <> (B \ X3)

        proof

          assume (B \ X1) = (B \ X2) or (B \ X2) = (B \ X3) or (B \ X1) = (B \ X3);

          then X2 = {} or X3 = {} or X3 = {} by A22, A27, A37, XBOOLE_1: 38, XBOOLE_1: 106;

          hence contradiction by A23, A28;

        end;

        consider A3 be POINT of ( G_ (k,X)) such that

         A39: A3 = (F . B3);

        

         A40: (B \ X3) c= B by XBOOLE_1: 106;

        then B3 in (F " K) by A18, A30, A31;

        then

         A41: A3 in K by A39, FUNCT_1:def 7;

        then

         A42: ex A13 be Subset of X st A3 = A13 & ( card A13) = k & S c= A13 by A35;

        

         A43: (B \ X1) c= B by XBOOLE_1: 106;

        then B1 in (F " K) by A18, A21, A33;

        then

         A44: A1 in K by A36, FUNCT_1:def 7;

        then

         A45: ex A11 be Subset of X st A1 = A11 & ( card A11) = k & S c= A11 by A35;

        then

         A46: ( card A1) = ((k - 1) + 1);

        consider A2 be POINT of ( G_ (k,X)) such that

         A47: A2 = (F . B2);

        

         A48: (B \ X2) c= B by XBOOLE_1: 106;

        then B2 in (F " K) by A18, A25, A26;

        then

         A49: A2 in K by A47, FUNCT_1:def 7;

        then

        consider L3a be LINE of ( G_ (k,X)) such that

         A50: {A1, A2} on L3a by A11, A44;

        

         A51: ( card A1) = ((k + 1) - 1) by A45;

        

         A52: F is incidence_preserving by A3;

        

         A53: ( card ((A1 /\ A2) /\ A3)) c= ( card (A1 /\ A2)) by CARD_1: 11, XBOOLE_1: 17;

        consider L1 be LINE of ( G_ (k,X)) such that

         A54: L1 = (F . L2);

        B1 on L2 by A1, A12, A43, A33, A32, Th10;

        then

         A55: A1 on L1 by A52, A36, A54;

        then

         A56: A1 c= L1 by A1, A12, Th10;

        L1 in the Lines of ( G_ (k,X));

        then

         A57: ex l12 be Subset of X st L1 = l12 & ( card l12) = (k + 1) by A14;

        B3 on L2 by A1, A12, A40, A31, A32, Th10;

        then

         A58: A3 on L1 by A52, A39, A54;

        then

         A59: A3 c= L1 by A1, A12, Th10;

        then (A1 \/ A3) c= L1 by A56, XBOOLE_1: 8;

        then

         A60: ( card (A1 \/ A3)) c= (k + 1) by A57, CARD_1: 11;

        

         A61: ex A12 be Subset of X st A2 = A12 & ( card A12) = k & S c= A12 by A49, A35;

        then

         A62: ( card A2) = ((k - 1) + 1);

        B2 on L2 by A1, A12, A48, A26, A32, Th10;

        then

         A63: A2 on L1 by A52, A47, A54;

        then

         A64: A2 c= L1 by A1, A12, Th10;

        then (A1 \/ A2) c= L1 by A56, XBOOLE_1: 8;

        then

         A65: ( card (A1 \/ A2)) c= (k + 1) by A57, CARD_1: 11;

        

         A66: the point-map of F is bijective & the Points of ( G_ (k,X)) = ( dom the point-map of F) by A3, FUNCT_2: 52;

        then

         A67: A1 <> A2 by A38, A33, A26, A36, A47, FUNCT_1:def 4;

        then (k + 1) c= ( card (A1 \/ A2)) by A45, A61, Th1;

        then ( card (A1 \/ A2)) = ((k - 1) + (2 * 1)) by A65, XBOOLE_0:def 10;

        then

         A68: ( card (A1 /\ A2)) = ((k + 1) - 2) by A4, A61, A46, Th2;

         {A1, A2} on L1 by A55, A63, INCSP_1: 1;

        then

         A69: L1 = L3a by A67, A50, INCSP_1:def 10;

        consider L3b be LINE of ( G_ (k,X)) such that

         A70: {A2, A3} on L3b by A11, A49, A41;

        A1 <> A3 by A66, A38, A33, A31, A36, A39, FUNCT_1:def 4;

        then (k + 1) c= ( card (A1 \/ A3)) by A45, A42, Th1;

        then ( card (A1 \/ A3)) = ((k - 1) + (2 * 1)) by A60, XBOOLE_0:def 10;

        then

         A71: ( card (A1 /\ A3)) = ((k + 1) - 2) by A4, A42, A46, Th2;

        A3 on L3b by A70, INCSP_1: 1;

        then

         A72: A3 c= L3b by A1, A12, Th10;

        A2 on L3b by A70, INCSP_1: 1;

        then

         A73: A2 c= L3b by A1, A12, Th10;

        L3b in the Lines of ( G_ (k,X));

        then

         A74: ex l13b be Subset of X st L3b = l13b & ( card l13b) = (k + 1) by A14;

        ( card (A1 /\ A2)) in ( succ (k - 1)) by A5, A67, A45, A61, Th1;

        then ( card (A1 /\ A2)) c= m by A24, ORDINAL1: 22;

        then

         A75: ( card ((A1 /\ A2) /\ A3)) c= m by A53;

        S c= (A1 /\ A2) by A45, A61, XBOOLE_1: 19;

        then S c= ((A1 /\ A2) /\ A3) by A42, XBOOLE_1: 19;

        then m c= ( card ((A1 /\ A2) /\ A3)) by A34, A24, CARD_1: 11;

        then

         A76: (k - 1) = ( card ((A1 /\ A2) /\ A3)) by A24, A75, XBOOLE_0:def 10;

        A1 on L3a by A50, INCSP_1: 1;

        then

         A77: A1 c= L3a by A1, A12, Th10;

        

         A78: (k - 1) <> ((k + 1) - 3);

        (A2 \/ A3) c= L1 by A64, A59, XBOOLE_1: 8;

        then

         A79: ( card (A2 \/ A3)) c= (k + 1) by A57, CARD_1: 11;

        

         A80: A2 <> A3 by A66, A38, A26, A31, A47, A39, FUNCT_1:def 4;

        then (k + 1) c= ( card (A2 \/ A3)) by A61, A42, Th1;

        then ( card (A2 \/ A3)) = ((k - 1) + (2 * 1)) by A79, XBOOLE_0:def 10;

        then

         A81: ( card (A2 /\ A3)) = ((k + 1) - 2) by A4, A42, A62, Th2;

        (2 + 1) <= (k + 1) & 2 <= (k + 1) by A1, A15, XREAL_1: 6, XXREAL_0: 2;

        then

         A82: ( card ((A1 \/ A2) \/ A3)) = ((k + 1) + 1) by A61, A42, A76, A68, A51, A81, A71, A78, Th7;

        

         A83: L3a <> L3b

        proof

          assume L3a = L3b;

          then (A1 \/ A2) c= L3b by A77, A73, XBOOLE_1: 8;

          then ((A1 \/ A2) \/ A3) c= L3b by A72, XBOOLE_1: 8;

          then ( Segm (k + 2)) c= ( Segm (k + 1)) by A82, A74, CARD_1: 11;

          then (k + 2) <= (k + 1) by NAT_1: 39;

          hence contradiction by XREAL_1: 6;

        end;

         {A2, A3} on L1 by A63, A58, INCSP_1: 1;

        hence contradiction by A80, A70, A83, A69, INCSP_1:def 10;

      end;

      

       A84: not (F .: K) is TOP

      proof

        

         A85: (k - 1) <> ((k + 1) - 3);

        assume (F .: K) is TOP;

        then

        consider B be Subset of X such that

         A86: ( card B) = (k + 1) & (F .: K) = { A where A be Subset of X : ( card A) = k & A c= B };

        B in the Lines of ( G_ (k,X)) by A14, A86;

        then

        consider L2 be LINE of ( G_ (k,X)) such that

         A87: B = L2;

        the line-map of F is bijective by A3;

        then the Lines of ( G_ (k,X)) = ( rng the line-map of F) by FUNCT_2:def 3;

        then

        consider l1 be object such that

         A88: l1 in ( dom the line-map of F) and

         A89: L2 = (the line-map of F . l1) by FUNCT_1:def 3;

        consider L1 be LINE of ( G_ (k,X)) such that

         A90: l1 = L1 by A88;

        

         A91: L2 = (F . L1) by A89, A90;

        consider X1 be set such that

         A92: X1 c= B & ( card X1) = 1 by A16, A86, CARD_FIL: 36;

        

         A93: B is finite by A86;

        then

         A94: ( card (B \ X1)) = ((k + 1) - 1) by A86, A92, CARD_2: 44;

        then

        consider X2 be set such that

         A95: X2 c= (B \ X1) and

         A96: ( card X2) = 1 by A8, CARD_FIL: 36;

        consider m be Nat such that

         A97: m = (k - 1) by A4;

        ( card ((B \ X1) \ X2)) = (k - 1) by A93, A94, A95, A96, CARD_2: 44;

        then

        consider X3 be set such that

         A98: X3 c= ((B \ X1) \ X2) and

         A99: ( card X3) = 1 by A6, CARD_FIL: 36;

        

         A100: X3 c= (B \ (X2 \/ X1)) by A98, XBOOLE_1: 41;

        then

         A101: ( card (B \ X3)) = ((k + 1) - 1) by A86, A93, A99, CARD_2: 44, XBOOLE_1: 106;

        then (B \ X3) in the Points of ( G_ (k,X)) by A13;

        then

        consider B3 be POINT of ( G_ (k,X)) such that

         A102: (B \ X3) = B3;

        L1 in the Lines of ( G_ (k,X));

        then

         A103: ex l12 be Subset of X st L1 = l12 & ( card l12) = (k + 1) by A14;

        (B \ X1) in the Points of ( G_ (k,X)) by A13, A94;

        then

        consider B1 be POINT of ( G_ (k,X)) such that

         A104: (B \ X1) = B1;

        

         A105: (B \ X1) c= B by XBOOLE_1: 106;

        then

         A106: B1 on L2 by A1, A12, A104, A87, Th10;

        consider S be Subset of X such that

         A107: ( card S) = (k - 1) and

         A108: K = { A where A be Subset of X : ( card A) = k & S c= A } by A9;

        

         A109: F is incidence_preserving by A3;

        

         A110: (B \ X3) c= B by XBOOLE_1: 106;

        then

         A111: B3 on L2 by A1, A12, A102, A87, Th10;

        

         A112: the point-map of F is bijective by A3;

        then

         A113: the Points of ( G_ (k,X)) = ( rng the point-map of F) by FUNCT_2:def 3;

        then

        consider a3 be object such that

         A114: a3 in ( dom the point-map of F) and

         A115: B3 = (the point-map of F . a3) by FUNCT_1:def 3;

        consider A3 be POINT of ( G_ (k,X)) such that

         A116: a3 = A3 by A114;

        consider a1 be object such that

         A117: a1 in ( dom the point-map of F) and

         A118: B1 = (the point-map of F . a1) by A113, FUNCT_1:def 3;

        consider A1 be POINT of ( G_ (k,X)) such that

         A119: a1 = A1 by A117;

        B3 in (F .: K) by A86, A101, A110, A102;

        then ex C3 be object st C3 in ( dom the point-map of F) & C3 in K & B3 = (the point-map of F . C3) by FUNCT_1:def 6;

        then

         A120: A3 in K by A112, A114, A115, A116, FUNCT_1:def 4;

        then

         A121: ex A13 be Subset of X st A3 = A13 & ( card A13) = k & S c= A13 by A108;

        B1 in (F .: K) by A86, A94, A105, A104;

        then ex C1 be object st C1 in ( dom the point-map of F) & C1 in K & B1 = (the point-map of F . C1) by FUNCT_1:def 6;

        then

         A122: A1 in K by A112, A117, A118, A119, FUNCT_1:def 4;

        then

         A123: ex A11 be Subset of X st A1 = A11 & ( card A11) = k & S c= A11 by A108;

        then

         A124: ( card A1) = ((k - 1) + 1);

        

         A125: B1 = (F . A1) by A118, A119;

        then A1 on L1 by A109, A106, A91;

        then

         A126: A1 c= L1 by A1, A12, Th10;

        

         A127: B3 = (F . A3) by A115, A116;

        then A3 on L1 by A109, A111, A91;

        then

         A128: A3 c= L1 by A1, A12, Th10;

        then (A1 \/ A3) c= L1 by A126, XBOOLE_1: 8;

        then

         A129: ( card (A1 \/ A3)) c= (k + 1) by A103, CARD_1: 11;

        

         A130: X3 c= ((B \ X2) \ X1) by A100, XBOOLE_1: 41;

        

         A131: (B \ X1) <> (B \ X2) & (B \ X2) <> (B \ X3) & (B \ X1) <> (B \ X3)

        proof

          assume (B \ X1) = (B \ X2) or (B \ X2) = (B \ X3) or (B \ X1) = (B \ X3);

          then X2 = {} or X3 = {} or X3 = {} by A95, A98, A130, XBOOLE_1: 38, XBOOLE_1: 106;

          hence contradiction by A96, A99;

        end;

        then (k + 1) c= ( card (A1 \/ A3)) by A104, A102, A118, A115, A119, A116, A123, A121, Th1;

        then ( card (A1 \/ A3)) = ((k - 1) + (2 * 1)) by A129, XBOOLE_0:def 10;

        then

         A132: ( card (A1 /\ A3)) = ((k + 1) - 2) by A4, A121, A124, Th2;

        

         A133: ( card (B \ X2)) = ((k + 1) - 1) by A86, A93, A95, A96, CARD_2: 44, XBOOLE_1: 106;

        then (B \ X2) in the Points of ( G_ (k,X)) by A13;

        then

        consider B2 be POINT of ( G_ (k,X)) such that

         A134: (B \ X2) = B2;

        

         A135: (B \ X2) c= B by XBOOLE_1: 106;

        then

         A136: B2 on L2 by A1, A12, A134, A87, Th10;

        consider a2 be object such that

         A137: a2 in ( dom the point-map of F) and

         A138: B2 = (the point-map of F . a2) by A113, FUNCT_1:def 3;

        consider A2 be POINT of ( G_ (k,X)) such that

         A139: a2 = A2 by A137;

        B2 in (F .: K) by A86, A133, A135, A134;

        then ex C2 be object st C2 in ( dom the point-map of F) & C2 in K & B2 = (the point-map of F . C2) by FUNCT_1:def 6;

        then

         A140: A2 in K by A112, A137, A138, A139, FUNCT_1:def 4;

        then

         A141: ex A12 be Subset of X st A2 = A12 & ( card A12) = k & S c= A12 by A108;

        then

         A142: ( card A2) = ((k - 1) + 1);

        

         A143: B2 = (F . A2) by A138, A139;

        then A2 on L1 by A109, A136, A91;

        then

         A144: A2 c= L1 by A1, A12, Th10;

        then (A1 \/ A2) c= L1 by A126, XBOOLE_1: 8;

        then

         A145: ( card (A1 \/ A2)) c= (k + 1) by A103, CARD_1: 11;

        (k + 1) c= ( card (A1 \/ A2)) by A131, A104, A134, A118, A138, A119, A139, A123, A141, Th1;

        then ( card (A1 \/ A2)) = ((k - 1) + (2 * 1)) by A145, XBOOLE_0:def 10;

        then

         A146: ( card (A1 /\ A2)) = ((k + 1) - 2) by A4, A141, A124, Th2;

        

         A147: A2 on L1 by A109, A136, A143, A91;

        (A2 \/ A3) c= L1 by A144, A128, XBOOLE_1: 8;

        then

         A148: ( card (A2 \/ A3)) c= (k + 1) by A103, CARD_1: 11;

        (k + 1) c= ( card (A2 \/ A3)) by A131, A134, A102, A138, A115, A139, A116, A141, A121, Th1;

        then ( card (A2 \/ A3)) = ((k - 1) + (2 * 1)) by A148, XBOOLE_0:def 10;

        then

         A149: ( card (A2 /\ A3)) = ((k + 1) - 2) by A4, A121, A142, Th2;

        

         A150: ( card A1) = ((k + 1) - 1) by A123;

        consider L3a be LINE of ( G_ (k,X)) such that

         A151: {A1, A2} on L3a by A11, A122, A140;

        ( card (A1 /\ A2)) in k by A131, A104, A134, A118, A138, A119, A139, A123, A141, Th1;

        then

         A152: ( card (A1 /\ A2)) c= m by A5, A97, ORDINAL1: 22;

        ( card ((A1 /\ A2) /\ A3)) c= ( card (A1 /\ A2)) by CARD_1: 11, XBOOLE_1: 17;

        then

         A153: ( card ((A1 /\ A2) /\ A3)) c= m by A152;

        S c= (A1 /\ A2) by A123, A141, XBOOLE_1: 19;

        then S c= ((A1 /\ A2) /\ A3) by A121, XBOOLE_1: 19;

        then m c= ( card ((A1 /\ A2) /\ A3)) by A107, A97, CARD_1: 11;

        then

         A154: (k - 1) = ( card ((A1 /\ A2) /\ A3)) by A97, A153, XBOOLE_0:def 10;

        A1 on L3a by A151, INCSP_1: 1;

        then

         A155: A1 c= L3a by A1, A12, Th10;

        consider L3b be LINE of ( G_ (k,X)) such that

         A156: {A2, A3} on L3b by A11, A140, A120;

        A3 on L3b by A156, INCSP_1: 1;

        then

         A157: A3 c= L3b by A1, A12, Th10;

        A2 on L3b by A156, INCSP_1: 1;

        then

         A158: A2 c= L3b by A1, A12, Th10;

        L3b in the Lines of ( G_ (k,X));

        then

         A159: ex l13b be Subset of X st L3b = l13b & ( card l13b) = (k + 1) by A14;

        (2 + 1) <= (k + 1) & 2 <= (k + 1) by A1, A15, XREAL_1: 6, XXREAL_0: 2;

        then

         A160: ( card ((A1 \/ A2) \/ A3)) = ((k + 1) + 1) by A141, A121, A154, A146, A150, A149, A132, A85, Th7;

        

         A161: L3a <> L3b

        proof

          assume L3a = L3b;

          then (A1 \/ A2) c= L3b by A155, A158, XBOOLE_1: 8;

          then ((A1 \/ A2) \/ A3) c= L3b by A157, XBOOLE_1: 8;

          then ( Segm (k + 2)) c= ( Segm (k + 1)) by A160, A159, CARD_1: 11;

          then (k + 2) <= (k + 1) by NAT_1: 39;

          hence contradiction by XREAL_1: 6;

        end;

        A1 on L1 by A109, A106, A125, A91;

        then {A1, A2} on L1 by A147, INCSP_1: 1;

        then

         A162: L1 = L3a by A131, A104, A134, A118, A138, A119, A139, A151, INCSP_1:def 10;

        A3 on L1 by A109, A111, A127, A91;

        then {A2, A3} on L1 by A147, INCSP_1: 1;

        hence contradiction by A131, A134, A102, A138, A115, A139, A116, A156, A161, A162, INCSP_1:def 10;

      end;

      (F .: K) is maximal_clique & (F " K) is maximal_clique by A3, A10, Th22;

      hence thesis by A1, A2, A84, A17, Th15;

    end;

    definition

      let k be Nat;

      let X be non empty set;

      let s be Permutation of X;

      :: COMBGRAS:def14

      func incprojmap (k,s) -> strict IncProjMap over ( G_ (k,X)), ( G_ (k,X)) means

      : Def14: (for A be POINT of ( G_ (k,X)) holds (it . A) = (s .: A)) & for L be LINE of ( G_ (k,X)) holds (it . L) = (s .: L);

      existence

      proof

        deffunc F( set) = (s .: $1);

        consider P be Function such that

         A2: ( dom P) = the Points of ( G_ (k,X)) & for x st x in the Points of ( G_ (k,X)) holds (P . x) = F(x) from FUNCT_1:sch 5;

        

         A3: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A1, Def1;

        ( rng P) c= the Points of ( G_ (k,X))

        proof

          let b be object;

          reconsider bb = b as set by TARSKI: 1;

          assume b in ( rng P);

          then

          consider a be object such that

           A4: a in the Points of ( G_ (k,X)) and

           A5: b = (P . a) by A2, FUNCT_1:def 3;

          consider A be Subset of X such that

           A6: A = a and

           A7: ( card A) = k by A3, A4;

          

           A8: b = (s .: A) by A2, A4, A5, A6;

          

           A9: bb c= X

          proof

            let y be object;

            assume y in bb;

            then ex x be object st x in ( dom s) & x in A & y = (s . x) by A8, FUNCT_1:def 6;

            then y in ( rng s) by FUNCT_1: 3;

            hence thesis by FUNCT_2:def 3;

          end;

          ( dom s) = X by FUNCT_2:def 1;

          then ( card bb) = k by A7, A8, Th4;

          hence thesis by A3, A9;

        end;

        then

        reconsider P as Function of the Points of ( G_ (k,X)), the Points of ( G_ (k,X)) by A2, FUNCT_2: 2;

        

         A10: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, Def1;

        consider L be Function such that

         A11: ( dom L) = the Lines of ( G_ (k,X)) & for x st x in the Lines of ( G_ (k,X)) holds (L . x) = F(x) from FUNCT_1:sch 5;

        ( rng L) c= the Lines of ( G_ (k,X))

        proof

          let b be object;

          reconsider bb = b as set by TARSKI: 1;

          assume b in ( rng L);

          then

          consider a be object such that

           A12: a in the Lines of ( G_ (k,X)) and

           A13: b = (L . a) by A11, FUNCT_1:def 3;

          consider A be Subset of X such that

           A14: A = a and

           A15: ( card A) = (k + 1) by A10, A12;

          

           A16: b = (s .: A) by A11, A12, A13, A14;

          

           A17: bb c= X

          proof

            let y be object;

            assume y in bb;

            then ex x be object st x in ( dom s) & x in A & y = (s . x) by A16, FUNCT_1:def 6;

            then y in ( rng s) by FUNCT_1: 3;

            hence thesis by FUNCT_2:def 3;

          end;

          ( dom s) = X by FUNCT_2:def 1;

          then ( card bb) = (k + 1) by A15, A16, Th4;

          hence thesis by A10, A17;

        end;

        then

        reconsider L as Function of the Lines of ( G_ (k,X)), the Lines of ( G_ (k,X)) by A11, FUNCT_2: 2;

        take IncProjMap (# P, L #);

        thus thesis by A2, A11;

      end;

      uniqueness

      proof

        let f1,f2 be strict IncProjMap over ( G_ (k,X)), ( G_ (k,X));

        assume that

         A18: for A be POINT of ( G_ (k,X)) holds (f1 . A) = (s .: A) and

         A19: for L be LINE of ( G_ (k,X)) holds (f1 . L) = (s .: L) and

         A20: for A be POINT of ( G_ (k,X)) holds (f2 . A) = (s .: A) and

         A21: for L be LINE of ( G_ (k,X)) holds (f2 . L) = (s .: L);

        

         A22: for L be LINE of ( G_ (k,X)) holds (f1 . L) = (f2 . L)

        proof

          let L be LINE of ( G_ (k,X));

          (f1 . L) = (s .: L) by A19;

          hence thesis by A21;

        end;

        for A be POINT of ( G_ (k,X)) holds (f1 . A) = (f2 . A)

        proof

          let A be POINT of ( G_ (k,X));

          (f1 . A) = (s .: A) by A18;

          hence thesis by A20;

        end;

        hence thesis by A22, Th16;

      end;

    end

    theorem :: COMBGRAS:24

    

     Th24: for k be Nat holds for X be non empty set st k = 1 & (k + 1) c= ( card X) holds for F be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) st F is automorphism holds ex s be Permutation of X st the IncProjMap of F = ( incprojmap (k,s))

    proof

      deffunc CH( object) = {$1};

      let k be Nat;

      let X be non empty set such that

       A1: k = 1 & (k + 1) c= ( card X);

      

       A2: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = 1 } by A1, Def1;

      consider c be Function such that

       A3: ( dom c) = X and

       A4: for x be object st x in X holds (c . x) = CH(x) from FUNCT_1:sch 3;

      

       A5: ( rng c) c= the Points of ( G_ (k,X))

      proof

        let y be object;

        assume y in ( rng c);

        then

        consider x be object such that

         A6: x in ( dom c) & y = (c . x) by FUNCT_1:def 3;

        

         A7: ( card {x}) = 1 by CARD_1: 30;

         {x} c= X & y = {x} by A3, A4, A6, ZFMISC_1: 31;

        hence thesis by A2, A7;

      end;

      let F be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) such that

       A8: F is automorphism;

      

       A9: the point-map of F is bijective by A8;

      reconsider c as Function of X, the Points of ( G_ (k,X)) by A3, A5, FUNCT_2: 2;

      deffunc W( Element of X) = ( union (F . (c . $1)));

      consider f be Function such that

       A10: ( dom f) = X and

       A11: for x be Element of X holds (f . x) = W(x) from FUNCT_1:sch 4;

      ( rng f) c= X

      proof

        let b be object;

        assume b in ( rng f);

        then

        consider a be object such that

         A12: a in X and

         A13: b = (f . a) by A10, FUNCT_1:def 3;

        reconsider a as Element of X by A12;

        

         A14: b = ( union (F . (c . a))) by A11, A13;

        consider A be POINT of ( G_ (k,X)) such that

         A15: A = (F . (c . a));

        A in the Points of ( G_ (k,X));

        then

         A16: ex A1 be Subset of X st A1 = A & ( card A1) = 1 by A2;

        then

        consider x be object such that

         A17: A = {x} by CARD_2: 42;

        x in X by A16, A17, ZFMISC_1: 31;

        hence thesis by A14, A15, A17, ZFMISC_1: 25;

      end;

      then

      reconsider f as Function of X, X by A10, FUNCT_2: 2;

      

       A18: F is incidence_preserving by A8;

      

       A19: ( dom the point-map of F) = the Points of ( G_ (k,X)) by FUNCT_2: 52;

      

       A20: f is one-to-one

      proof

        let x1,x2 be object such that

         A21: x1 in ( dom f) & x2 in ( dom f) and

         A22: (f . x1) = (f . x2);

        reconsider x1, x2 as Element of X by A21;

        consider A1 be POINT of ( G_ (k,X)) such that

         A23: A1 = (F . (c . x1));

        A1 in the Points of ( G_ (k,X));

        then ex A11 be Subset of X st A11 = A1 & ( card A11) = 1 by A2;

        then

        consider y1 be object such that

         A24: A1 = {y1} by CARD_2: 42;

        

         A25: (c . x1) = {x1} & (c . x2) = {x2} by A4;

        consider A2 be POINT of ( G_ (k,X)) such that

         A26: A2 = (F . (c . x2));

        A2 in the Points of ( G_ (k,X));

        then ex A12 be Subset of X st A12 = A2 & ( card A12) = 1 by A2;

        then

        consider y2 be object such that

         A27: A2 = {y2} by CARD_2: 42;

        (f . x2) = ( union (F . (c . x2))) by A11;

        then

         A28: (f . x2) = y2 by A26, A27, ZFMISC_1: 25;

        (f . x1) = ( union (F . (c . x1))) by A11;

        then (f . x1) = y1 by A23, A24, ZFMISC_1: 25;

        then (c . x1) = (c . x2) by A9, A19, A22, A23, A26, A24, A27, A28, FUNCT_1:def 4;

        hence thesis by A25, ZFMISC_1: 3;

      end;

      

       A29: ( rng the point-map of F) = the Points of ( G_ (k,X)) by A9, FUNCT_2:def 3;

      for y be object st y in X holds ex x be object st x in X & y = (f . x)

      proof

        let y be object;

        assume y in X;

        then

         A30: {y} c= X by ZFMISC_1: 31;

        ( card {y}) = 1 by CARD_1: 30;

        then {y} in ( rng the point-map of F) by A2, A29, A30;

        then

        consider a be object such that

         A31: a in ( dom the point-map of F) and

         A32: {y} = (the point-map of F . a) by FUNCT_1:def 3;

        a in the Points of ( G_ (k,X)) by A31;

        then

         A33: ex A1 be Subset of X st A1 = a & ( card A1) = 1 by A2;

        then

        consider x be object such that

         A34: a = {x} by CARD_2: 42;

        reconsider x as Element of X by A33, A34, ZFMISC_1: 31;

         {y} = (F . (c . x)) by A4, A32, A34;

        then y = ( union (F . (c . x))) by ZFMISC_1: 25;

        then y = (f . x) by A11;

        hence thesis;

      end;

      then ( rng f) = X by FUNCT_2: 10;

      then f is onto by FUNCT_2:def 3;

      then

      reconsider f as Permutation of X by A20;

      

       A35: ( dom the line-map of F) = the Lines of ( G_ (k,X)) by FUNCT_2: 52;

      

       A36: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (1 + 1) } by A1, Def1;

      

       A37: for x be object st x in ( dom the line-map of F) holds (the line-map of F . x) = (the line-map of ( incprojmap (k,f)) . x)

      proof

        let x be object;

        assume

         A38: x in ( dom the line-map of F);

        then

        consider A be LINE of ( G_ (k,X)) such that

         A39: x = A;

        consider A11 be Subset of X such that

         A40: x = A11 and

         A41: ( card A11) = 2 by A36, A35, A38;

        consider x1,x2 be object such that

         A42: x1 <> x2 and

         A43: x = {x1, x2} by A40, A41, CARD_2: 60;

        reconsider x1, x2 as Element of X by A40, A43, ZFMISC_1: 32;

        (c . x1) = {x1} by A4;

        then

        consider A1 be POINT of ( G_ (k,X)) such that

         A44: A1 = {x1};

        (c . x2) = {x2} by A4;

        then

        consider A2 be POINT of ( G_ (k,X)) such that

         A45: A2 = {x2};

        A1 <> A2 by A42, A44, A45, ZFMISC_1: 18;

        then

         A46: (F . A1) <> (F . A2) by A9, A19, FUNCT_1:def 4;

        (F . A2) in the Points of ( G_ (k,X));

        then

         A47: ex B2 be Subset of X st B2 = (F . A2) & ( card B2) = 1 by A2;

        then

        consider y2 be object such that

         A48: (F . A2) = {y2} by CARD_2: 42;

        A1 c= A by A39, A43, A44, ZFMISC_1: 36;

        then A1 on A by A1, Th10;

        then (F . A1) on (F . A) by A18;

        then

         A49: (F . A1) c= (F . A) by A1, Th10;

        

         A50: (( incprojmap (k,f)) . A) = (f .: A) & (f .: (A1 \/ A2)) = ((f .: A1) \/ (f .: A2)) by A1, Def14, RELAT_1: 120;

        

         A51: (A1 \/ A2) = A by A39, A43, A44, A45, ENUMSET1: 1;

        (F . A1) in the Points of ( G_ (k,X));

        then

         A52: ex B1 be Subset of X st B1 = (F . A1) & ( card B1) = 1 by A2;

        then

         A53: ex y1 be object st (F . A1) = {y1} by CARD_2: 42;

        A2 c= A by A39, A43, A45, ZFMISC_1: 36;

        then A2 on A by A1, Th10;

        then (F . A2) on (F . A) by A18;

        then

         A54: (F . A2) c= (F . A) by A1, Th10;

        (F . (c . x2)) = (F . A2) by A4, A45;

        then

         A55: (f . x2) = ( union (F . A2)) by A11;

        ( Im (f,x2)) = {(f . x2)} by A10, FUNCT_1: 59;

        then

         A56: (f .: A2) = (F . A2) by A45, A55, A48, ZFMISC_1: 25;

        

         A57: (F . A1) is finite by A52;

         not y2 in (F . A1) by A46, A52, A47, A57, A48, CARD_2: 102, ZFMISC_1: 31;

        then

         A58: ( card ((F . A1) \/ (F . A2))) = (1 + 1) by A52, A53, A48, CARD_2: 41;

        (F . (c . x1)) = (F . A1) by A4, A44;

        then

         A59: (f . x1) = ( union (F . A1)) by A11;

        ( Im (f,x1)) = {(f . x1)} by A10, FUNCT_1: 59;

        then

         A60: (f .: A1) = (F . A1) by A44, A59, A53, ZFMISC_1: 25;

        (F . A) in the Lines of ( G_ (k,X));

        then

         A61: ex B3 be Subset of X st B3 = (F . A) & ( card B3) = 2 by A36;

        then (F . A) is finite;

        hence thesis by A39, A50, A51, A49, A54, A61, A58, A60, A56, CARD_2: 102, XBOOLE_1: 8;

      end;

      

       A62: for x be object st x in ( dom the point-map of F) holds (the point-map of F . x) = (the point-map of ( incprojmap (k,f)) . x)

      proof

        let x be object;

        assume

         A63: x in ( dom the point-map of F);

        then

        consider A be POINT of ( G_ (k,X)) such that

         A64: x = A;

        

         A65: ex A1 be Subset of X st x = A1 & ( card A1) = 1 by A2, A19, A63;

        then

        consider x1 be object such that

         A66: x = {x1} by CARD_2: 42;

        reconsider x1 as Element of X by A65, A66, ZFMISC_1: 31;

        (F . (c . x1)) = (F . A) by A4, A64, A66;

        then

         A67: (f . x1) = ( union (F . A)) by A11;

        (F . A) in the Points of ( G_ (k,X));

        then

        consider B be Subset of X such that

         A68: B = (F . A) and

         A69: ( card B) = 1 by A2;

        

         A70: ex x2 be object st B = {x2} by A69, CARD_2: 42;

        (( incprojmap (k,f)) . A) = (f .: A) & ( Im (f,x1)) = {(f . x1)} by A1, A10, Def14, FUNCT_1: 59;

        hence thesis by A64, A66, A67, A68, A70, ZFMISC_1: 25;

      end;

      ( dom the point-map of ( incprojmap (k,f))) = the Points of ( G_ (k,X)) by FUNCT_2: 52;

      then

       A71: the point-map of F = the point-map of ( incprojmap (k,f)) by A19, A62;

      ( dom the line-map of ( incprojmap (k,f))) = the Lines of ( G_ (k,X)) by FUNCT_2: 52;

      then the IncProjMap of F = ( incprojmap (k,f)) by A35, A71, A37, FUNCT_1:def 11;

      hence thesis;

    end;

    theorem :: COMBGRAS:25

    

     Th25: for k be Nat holds for X be non empty set st 1 < k & ( card X) = (k + 1) holds for F be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) st F is automorphism holds ex s be Permutation of X st the IncProjMap of F = ( incprojmap (k,s))

    proof

      let k be Nat;

      let X be non empty set such that

       A1: 1 < k and

       A2: (k + 1) = ( card X);

      deffunc CH( object) = (X \ {$1});

      consider c be Function such that

       A3: ( dom c) = X and

       A4: for x be object st x in X holds (c . x) = CH(x) from FUNCT_1:sch 3;

      

       A5: X is finite by A2;

      

       A6: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A1, A2, Def1;

      

       A7: ( rng c) c= the Points of ( G_ (k,X))

      proof

        let y be object;

        assume y in ( rng c);

        then

        consider x be object such that

         A8: x in ( dom c) and

         A9: y = (c . x) by FUNCT_1:def 3;

        

         A10: ( card {x}) = 1 by CARD_1: 30;

         {x} c= X by A3, A8, ZFMISC_1: 31;

        then

         A11: ( card (X \ {x})) = ((k + 1) - 1) by A2, A5, A10, CARD_2: 44;

        y = (X \ {x}) by A3, A4, A8, A9;

        hence thesis by A6, A11;

      end;

      let F be IncProjMap over ( G_ (k,X)), ( G_ (k,X));

      assume F is automorphism;

      then

       A12: the point-map of F is bijective;

      reconsider c as Function of X, the Points of ( G_ (k,X)) by A3, A7, FUNCT_2: 2;

      deffunc W( Element of X) = ( union (X \ (F . (c . $1))));

      consider f be Function such that

       A13: ( dom f) = X and

       A14: for x be Element of X holds (f . x) = W(x) from FUNCT_1:sch 4;

      ( rng f) c= X

      proof

        let b be object;

        assume b in ( rng f);

        then

        consider a be object such that

         A15: a in X and

         A16: b = (f . a) by A13, FUNCT_1:def 3;

        reconsider a as Element of X by A15;

        

         A17: b = ( union (X \ (F . (c . a)))) by A14, A16;

        consider A be POINT of ( G_ (k,X)) such that

         A18: A = (F . (c . a));

        A in the Points of ( G_ (k,X));

        then ex A1 be Subset of X st A1 = A & ( card A1) = k by A6;

        then ( card (X \ A)) = ((k + 1) - k) by A2, A5, CARD_2: 44;

        then

        consider x be object such that

         A19: (X \ A) = {x} by CARD_2: 42;

        x in X by A19, ZFMISC_1: 31;

        hence thesis by A17, A18, A19, ZFMISC_1: 25;

      end;

      then

      reconsider f as Function of X, X by A13, FUNCT_2: 2;

      

       A20: ( dom the point-map of F) = the Points of ( G_ (k,X)) by FUNCT_2: 52;

      

       A21: f is one-to-one

      proof

        let x1,x2 be object such that

         A22: x1 in ( dom f) & x2 in ( dom f) and

         A23: (f . x1) = (f . x2);

        reconsider x1, x2 as Element of X by A22;

        consider A1 be POINT of ( G_ (k,X)) such that

         A24: A1 = (F . (c . x1));

        consider A2 be POINT of ( G_ (k,X)) such that

         A25: A2 = (F . (c . x2));

        A2 in the Points of ( G_ (k,X));

        then

         A26: ex A12 be Subset of X st A12 = A2 & ( card A12) = k by A6;

        then ( card (X \ A2)) = ((k + 1) - k) by A2, A5, CARD_2: 44;

        then

        consider y2 be object such that

         A27: (X \ A2) = {y2} by CARD_2: 42;

        A1 in the Points of ( G_ (k,X));

        then

         A28: ex A11 be Subset of X st A11 = A1 & ( card A11) = k by A6;

        then ( card (X \ A1)) = ((k + 1) - k) by A2, A5, CARD_2: 44;

        then

        consider y1 be object such that

         A29: (X \ A1) = {y1} by CARD_2: 42;

        (f . x2) = ( union (X \ (F . (c . x2)))) by A14;

        then

         A30: (f . x2) = y2 by A25, A27, ZFMISC_1: 25;

        (f . x1) = ( union (X \ (F . (c . x1)))) by A14;

        then (f . x1) = y1 by A24, A29, ZFMISC_1: 25;

        then A1 = A2 by A23, A28, A26, A29, A27, A30, Th5;

        then

         A31: (c . x1) = (c . x2) by A12, A20, A24, A25, FUNCT_1:def 4;

        (c . x1) = (X \ {x1}) & (c . x2) = (X \ {x2}) by A4;

        then {x1} = {x2} by A31, Th5;

        hence thesis by ZFMISC_1: 3;

      end;

      

       A32: ( rng the point-map of F) = the Points of ( G_ (k,X)) by A12, FUNCT_2:def 3;

      for y be object st y in X holds ex x be object st x in X & y = (f . x)

      proof

        let y be object;

        assume y in X;

        then

         A33: {y} c= X by ZFMISC_1: 31;

        ( card {y}) = 1 by CARD_1: 30;

        then ( card (X \ {y})) = ((k + 1) - 1) by A2, A5, A33, CARD_2: 44;

        then (X \ {y}) in ( rng the point-map of F) by A6, A32;

        then

        consider a be object such that

         A34: a in ( dom the point-map of F) and

         A35: (X \ {y}) = (the point-map of F . a) by FUNCT_1:def 3;

        reconsider a as set by TARSKI: 1;

        a in the Points of ( G_ (k,X)) by A34;

        then

         A36: ex A1 be Subset of X st A1 = a & ( card A1) = k by A6;

        then ( card (X \ a)) = ((k + 1) - k) by A2, A5, CARD_2: 44;

        then

        consider x be object such that

         A37: (X \ a) = {x} by CARD_2: 42;

        reconsider x as Element of X by A37, ZFMISC_1: 31;

        (a /\ X) = (X \ {x}) by A37, XBOOLE_1: 48;

        then

         A38: (X \ {x}) = a by A36, XBOOLE_1: 28;

        (c . x) = (X \ {x}) by A4;

        then (X /\ {y}) = (X \ (F . (c . x))) by A35, A38, XBOOLE_1: 48;

        then {y} = (X \ (F . (c . x))) by A33, XBOOLE_1: 28;

        then y = ( union (X \ (F . (c . x)))) by ZFMISC_1: 25;

        then y = (f . x) by A14;

        hence thesis;

      end;

      then

       A39: ( rng f) = X by FUNCT_2: 10;

      then f is onto by FUNCT_2:def 3;

      then

      reconsider f as Permutation of X by A21;

      

       A40: ( dom the line-map of F) = the Lines of ( G_ (k,X)) by FUNCT_2: 52;

      

       A41: for x be object st x in ( dom the point-map of F) holds (the point-map of F . x) = (the point-map of ( incprojmap (k,f)) . x)

      proof

        let x be object;

        assume

         A42: x in ( dom the point-map of F);

        then

        consider A be POINT of ( G_ (k,X)) such that

         A43: x = A;

        (F . A) in the Points of ( G_ (k,X));

        then

         A44: ex B be Subset of X st B = (F . A) & ( card B) = k by A6;

        then ( card (X \ (F . A))) = ((k + 1) - k) by A2, A5, CARD_2: 44;

        then

         A45: ex x2 be object st (X \ (F . A)) = {x2} by CARD_2: 42;

        (X \ (X \ (F . A))) = ((F . A) /\ X) & ((F . A) /\ X) = (F . A) by A44, XBOOLE_1: 28, XBOOLE_1: 48;

        then

         A46: (F . A) = (X \ {( union (X \ (F . A)))}) by A45, ZFMISC_1: 25;

        

         A47: (f .: X) = X by A39, RELSET_1: 22;

        

         A48: ex A1 be Subset of X st x = A1 & ( card A1) = k by A6, A20, A42;

        then

         A49: (X \ (X \ A)) = (A /\ X) & (A /\ X) = A by A43, XBOOLE_1: 28, XBOOLE_1: 48;

        ( card (X \ A)) = ((k + 1) - k) by A2, A5, A43, A48, CARD_2: 44;

        then

        consider x1 be object such that

         A50: (X \ A) = {x1} by CARD_2: 42;

        reconsider x1 as Element of X by A50, ZFMISC_1: 31;

        

         A51: (c . x1) = (X \ {x1}) & ( Im (f,x1)) = {(f . x1)} by A4, A13, FUNCT_1: 59;

        (( incprojmap (k,f)) . A) = (f .: A) by A1, A2, Def14;

        then (( incprojmap (k,f)) . A) = ((f .: X) \ (f .: {x1})) by A50, A49, FUNCT_1: 64;

        hence thesis by A14, A43, A50, A46, A49, A51, A47;

      end;

      ( dom the point-map of ( incprojmap (k,f))) = the Points of ( G_ (k,X)) by FUNCT_2: 52;

      then

       A52: the point-map of F = the point-map of ( incprojmap (k,f)) by A20, A41;

      

       A53: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, A2, Def1;

      

       A54: for x be object st x in ( dom the line-map of F) holds (the line-map of F . x) = (the line-map of ( incprojmap (k,f)) . x)

      proof

        let x be object;

        assume

         A55: x in ( dom the line-map of F);

        then

        consider A be LINE of ( G_ (k,X)) such that

         A56: x = A;

        (F . A) in the Lines of ( G_ (k,X));

        then ex y be Subset of X st y = (F . A) & ( card y) = (k + 1) by A53;

        then

         A57: (F . A) = X by A2, A5, CARD_2: 102;

        ex A11 be Subset of X st x = A11 & ( card A11) = (k + 1) by A53, A40, A55;

        then

         A58: x = X by A2, A5, CARD_2: 102;

        reconsider xx = x as set by TARSKI: 1;

        (( incprojmap (k,f)) . A) = (f .: xx) by A1, A2, A56, Def14;

        hence thesis by A39, A56, A58, A57, RELSET_1: 22;

      end;

      ( dom the line-map of ( incprojmap (k,f))) = the Lines of ( G_ (k,X)) by FUNCT_2: 52;

      then the IncProjMap of F = ( incprojmap (k,f)) by A40, A52, A54, FUNCT_1:def 11;

      hence thesis;

    end;

    theorem :: COMBGRAS:26

    

     Th26: for k be Element of NAT holds for X be non empty set st 0 < k & (k + 1) c= ( card X) holds for T be Subset of the Points of ( G_ (k,X)) holds for S be Subset of X holds ( card S) = (k - 1) & T = { A where A be Subset of X : ( card A) = k & S c= A } implies S = ( meet T)

    proof

      let k be Element of NAT ;

      let X be non empty set such that

       A1: 0 < k and

       A2: (k + 1) c= ( card X);

      (k - 1) is Element of NAT by A1, NAT_1: 20;

      then

      reconsider k1 = (k - 1) as Nat;

      let T be Subset of the Points of ( G_ (k,X));

      let S be Subset of X;

      assume that

       A3: ( card S) = (k - 1) and

       A4: T = { A where A be Subset of X : ( card A) = k & S c= A };

      

       A5: S is finite by A1, A3, NAT_1: 20;

      

       A6: T <> {}

      proof

        (X \ S) <> {}

        proof

          assume (X \ S) = {} ;

          then X c= S by XBOOLE_1: 37;

          then ( card X) = k1 by A3, XBOOLE_0:def 10;

          then ( Segm (k + 1)) c= ( Segm k1) by A2;

          then (1 + k) <= (( - 1) + k) by NAT_1: 39;

          hence contradiction by XREAL_1: 6;

        end;

        then

        consider x be object such that

         A7: x in (X \ S) by XBOOLE_0:def 1;

         {x} c= X by A7, ZFMISC_1: 31;

        then

         A8: S c= (S \/ {x}) & (S \/ {x}) c= X by XBOOLE_1: 7, XBOOLE_1: 8;

         not x in S by A7, XBOOLE_0:def 5;

        then ( card (S \/ {x})) = ((k - 1) + 1) by A3, A5, CARD_2: 41;

        then (S \/ {x}) in T by A4, A8;

        hence thesis;

      end;

      

       A9: ( meet T) c= S

      proof

        let y be object such that

         A10: y in ( meet T);

        y in S

        proof

          consider a1 be object such that

           A11: a1 in T by A6, XBOOLE_0:def 1;

          reconsider a1 as set by TARSKI: 1;

          

           A12: ex A1 be Subset of X st a1 = A1 & ( card A1) = k & S c= A1 by A4, A11;

          then

           A13: a1 is finite;

          (X \ a1) <> {}

          proof

            assume (X \ a1) = {} ;

            then X c= a1 by XBOOLE_1: 37;

            then ( card X) = k by A12, XBOOLE_0:def 10;

            then ( Segm (1 + k)) c= ( Segm ( 0 + k)) by A2;

            then (1 + k) <= ( 0 + k) by NAT_1: 39;

            hence contradiction by XREAL_1: 6;

          end;

          then

          consider y2 be object such that

           A14: y2 in (X \ a1) by XBOOLE_0:def 1;

          assume

           A15: not y in S;

          

           A16: S misses {y}

          proof

            assume not S misses {y};

            then (S /\ {y}) <> {} by XBOOLE_0:def 7;

            then

            consider z be object such that

             A17: z in (S /\ {y}) by XBOOLE_0:def 1;

            z in {y} & z in S by A17, XBOOLE_0:def 4;

            hence contradiction by A15, TARSKI:def 1;

          end;

          then S c= (a1 \ {y}) by A12, XBOOLE_1: 86;

          then

           A18: S c= ((a1 \ {y}) \/ {y2}) by XBOOLE_1: 10;

          

           A19: y in a1 by A10, A11, SETFAM_1:def 1;

          then y2 <> y by A14, XBOOLE_0:def 5;

          then

           A20: not y in {y2} by TARSKI:def 1;

          ( card {y}) = 1 & {y} c= a1 by A19, CARD_1: 30, ZFMISC_1: 31;

          then

           A21: ( card (a1 \ {y})) = (k - 1) by A12, A13, CARD_2: 44;

          then not y in (a1 \ {y}) by A3, A15, A12, A13, A16, CARD_2: 102, XBOOLE_1: 86;

          then

           A22: not y in ((a1 \ {y}) \/ {y2}) by A20, XBOOLE_0:def 3;

          

           A23: {y2} c= X by A14, ZFMISC_1: 31;

          (a1 \ {y}) c= X by A12, XBOOLE_1: 1;

          then

           A24: ((a1 \ {y}) \/ {y2}) c= X by A23, XBOOLE_1: 8;

           not y2 in (a1 \ {y}) by A14, XBOOLE_0:def 5;

          then ( card ((a1 \ {y}) \/ {y2})) = ((k - 1) + 1) by A13, A21, CARD_2: 41;

          then ((a1 \ {y}) \/ {y2}) in T by A4, A24, A18;

          hence contradiction by A10, A22, SETFAM_1:def 1;

        end;

        hence thesis;

      end;

      for a1 be set st a1 in T holds S c= a1

      proof

        let a1 be set;

        assume a1 in T;

        then ex A1 be Subset of X st a1 = A1 & ( card A1) = k & S c= A1 by A4;

        hence thesis;

      end;

      then S c= ( meet T) by A6, SETFAM_1: 5;

      hence thesis by A9, XBOOLE_0:def 10;

    end;

    theorem :: COMBGRAS:27

    for k be Element of NAT holds for X be non empty set st 0 < k & (k + 1) c= ( card X) holds for T be Subset of the Points of ( G_ (k,X)) st T is STAR holds for S be Subset of X holds S = ( meet T) implies ( card S) = (k - 1) & T = { A where A be Subset of X : ( card A) = k & S c= A }

    proof

      let k be Element of NAT ;

      let X be non empty set such that

       A1: 0 < k & (k + 1) c= ( card X);

      let T be Subset of the Points of ( G_ (k,X));

      assume T is STAR;

      then

      consider S1 be Subset of X such that

       A2: ( card S1) = (k - 1) & T = { A where A be Subset of X : ( card A) = k & S1 c= A };

      let S be Subset of X;

      assume

       A3: S = ( meet T);

      S1 = ( meet T) by A1, A2, Th26;

      hence thesis by A3, A2;

    end;

    theorem :: COMBGRAS:28

    

     Th28: for k be Element of NAT holds for X be non empty set st 0 < k & (k + 1) c= ( card X) holds for T1,T2 be Subset of the Points of ( G_ (k,X)) st T1 is STAR & T2 is STAR & ( meet T1) = ( meet T2) holds T1 = T2

    proof

      let k be Element of NAT ;

      let X be non empty set such that

       A1: 0 < k & (k + 1) c= ( card X);

      let T1,T2 be Subset of the Points of ( G_ (k,X)) such that

       A2: T1 is STAR and

       A3: T2 is STAR and

       A4: ( meet T1) = ( meet T2);

      consider S2 be Subset of X such that

       A5: ( card S2) = (k - 1) & T2 = { A where A be Subset of X : ( card A) = k & S2 c= A } by A3;

      

       A6: S2 = ( meet T2) by A1, A5, Th26;

      consider S1 be Subset of X such that

       A7: ( card S1) = (k - 1) & T1 = { A where A be Subset of X : ( card A) = k & S1 c= A } by A2;

      S1 = ( meet T1) by A1, A7, Th26;

      hence thesis by A4, A7, A5, A6;

    end;

    theorem :: COMBGRAS:29

    

     Th29: for k be Element of NAT holds for X be non empty set st (k + 1) c= ( card X) holds for A be finite Subset of X st ( card A) = (k - 1) holds ( ^^ (A,X,k)) is STAR

    proof

      let k be Element of NAT ;

      let X be non empty set such that

       A1: (k + 1) c= ( card X);

      let A be finite Subset of X such that

       A2: ( card A) = (k - 1);

      ( ^^ (A,X,k)) = ( ^^ (A,X)) by A1, A2, Def13;

      hence thesis by A2;

    end;

    theorem :: COMBGRAS:30

    

     Th30: for k be Element of NAT holds for X be non empty set st (k + 1) c= ( card X) holds for A be finite Subset of X st ( card A) = (k - 1) holds ( meet ( ^^ (A,X,k))) = A

    proof

      let k be Element of NAT ;

      let X be non empty set such that

       A1: (k + 1) c= ( card X);

      let A be finite Subset of X such that

       A2: ( card A) = (k - 1);

      ( ^^ (A,X,k)) = ( ^^ (A,X)) by A1, A2, Def13;

      hence thesis by A1, A2, Th26;

    end;

    theorem :: COMBGRAS:31

    

     Th31: for k be Nat holds for X be non empty set st 0 < k & (k + 3) c= ( card X) holds for F be IncProjMap over ( G_ ((k + 1),X)), ( G_ ((k + 1),X)) st F is automorphism holds ex H be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) st H is automorphism & the line-map of H = the point-map of F & for A be POINT of ( G_ (k,X)), B be finite set st B = A holds (H . A) = ( meet (F .: ( ^^ (B,X,(k + 1)))))

    proof

      let k be Nat;

      let X be non empty set such that

       A1: 0 < k and

       A2: (k + 3) c= ( card X);

      let F be IncProjMap over ( G_ ((k + 1),X)), ( G_ ((k + 1),X)) such that

       A3: F is automorphism;

      ( 0 + 2) < (k + (1 + 1)) by A1, XREAL_1: 6;

      then ( 0 + 2) < ((k + 1) + 1);

      then

       A4: 2 <= (k + 1) by NAT_1: 13;

      defpred P[ object, object] means ex B be finite set st B = $1 & $2 = ( meet (F .: ( ^^ (B,X,(k + 1)))));

      ((k + 1) + 0 ) <= ((k + 1) + 2) by XREAL_1: 6;

      then ( Segm (k + 1)) c= ( Segm (k + 3)) by NAT_1: 39;

      then

       A5: (k + 1) c= ( card X) by A2;

      then

       A6: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A1, Def1;

      

       A7: for e be object st e in the Points of ( G_ (k,X)) holds ex u be object st P[e, u]

      proof

        let e be object;

        assume e in the Points of ( G_ (k,X));

        then ex B be Subset of X st B = e & ( card B) = k by A6;

        then

        reconsider B = e as finite Subset of X;

        take ( meet (F .: ( ^^ (B,X,(k + 1)))));

        thus thesis;

      end;

      consider Hp be Function such that

       A8: ( dom Hp) = the Points of ( G_ (k,X)) and

       A9: for e be object st e in the Points of ( G_ (k,X)) holds P[e, (Hp . e)] from CLASSES1:sch 1( A7);

      

       A10: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, A5, Def1;

      ((k + 1) + 1) <= ((k + 1) + 2) by XREAL_1: 6;

      then ( Segm (k + 2)) c= ( Segm (k + 3)) by NAT_1: 39;

      then

       A11: ((k + 1) + 1) c= ( card X) by A2;

      then

       A12: the Points of ( G_ ((k + 1),X)) = { A where A be Subset of X : ( card A) = (k + 1) } by Def1;

      then

      reconsider Hl = the point-map of F as Function of the Lines of ( G_ (k,X)), the Lines of ( G_ (k,X)) by A10;

      

       A13: ((k + 1) + 2) c= ( card X) by A2;

      ( rng Hp) c= the Points of ( G_ (k,X))

      proof

        let y be object;

        assume y in ( rng Hp);

        then

        consider x be object such that

         A14: x in ( dom Hp) and

         A15: y = (Hp . x) by FUNCT_1:def 3;

        consider B be finite set such that

         A16: B = x and

         A17: y = ( meet (F .: ( ^^ (B,X,(k + 1))))) by A8, A9, A14, A15;

        

         A18: ex x1 be Subset of X st x = x1 & ( card x1) = k by A6, A8, A14;

        ( ^^ (B,X,(k + 1))) is STAR by A11, A16, A18, Th29;

        then (F .: ( ^^ (B,X,(k + 1)))) is STAR by A3, A4, A13, Th23;

        then

        consider S be Subset of X such that

         A19: ( card S) = ((k + 1) - 1) and

         A20: (F .: ( ^^ (B,X,(k + 1)))) = { C where C be Subset of X : ( card C) = (k + 1) & S c= C };

        S = ( meet (F .: ( ^^ (B,X,(k + 1))))) by A11, A19, A20, Th26;

        hence thesis by A6, A17, A19;

      end;

      then

      reconsider Hp as Function of the Points of ( G_ (k,X)), the Points of ( G_ (k,X)) by A8, FUNCT_2: 2;

      

       A21: the point-map of F is bijective by A3;

      

       A22: Hp is one-to-one

      proof

        let x1,x2 be object such that

         A23: x1 in ( dom Hp) and

         A24: x2 in ( dom Hp) and

         A25: (Hp . x1) = (Hp . x2);

        consider X2 be finite set such that

         A26: X2 = x2 and

         A27: (Hp . x2) = ( meet (F .: ( ^^ (X2,X,(k + 1))))) by A9, A24;

        

         A28: ex x12 be Subset of X st x2 = x12 & ( card x12) = k by A6, A8, A24;

        then

         A29: ( card X2) = ((k + 1) - 1) by A26;

        then

         A30: ( meet ( ^^ (X2,X,(k + 1)))) = X2 by A11, A26, A28, Th30;

        ( ^^ (X2,X,(k + 1))) is STAR by A11, A26, A28, Th29;

        then

         A31: (F .: ( ^^ (X2,X,(k + 1)))) is STAR by A3, A4, A13, Th23;

        consider X1 be finite set such that

         A32: X1 = x1 and

         A33: (Hp . x1) = ( meet (F .: ( ^^ (X1,X,(k + 1))))) by A9, A23;

        

         A34: ex x11 be Subset of X st x1 = x11 & ( card x11) = k by A6, A8, A23;

        ( ^^ (X1,X,(k + 1))) is STAR by A11, A32, A34, Th29;

        then

         A35: (F .: ( ^^ (X1,X,(k + 1)))) is STAR by A3, A4, A13, Th23;

        ( meet ( ^^ (X1,X,(k + 1)))) = X1 by A11, A32, A34, A29, Th30;

        hence thesis by A11, A21, A25, A32, A33, A26, A27, A35, A31, A30, Th6, Th28;

      end;

      take H = IncProjMap (# Hp, Hl #);

      

       A36: ( dom the point-map of F) = the Points of ( G_ ((k + 1),X)) by FUNCT_2: 52;

      

       A37: H is incidence_preserving

      proof

        let A1 be POINT of ( G_ (k,X));

        let L1 be LINE of ( G_ (k,X));

        

         A38: P[A1, (Hp . A1)] by A9;

        L1 in the Lines of ( G_ (k,X));

        then

         A39: ex l1 be Subset of X st l1 = L1 & ( card l1) = (k + 1) by A10;

        A1 in the Points of ( G_ (k,X));

        then

        consider a1 be Subset of X such that

         A40: a1 = A1 and

         A41: ( card a1) = k by A6;

        consider L11 be POINT of ( G_ ((k + 1),X)) such that

         A42: L11 = L1 by A10, A12;

        reconsider a1 as finite Subset of X by A41;

        

         A43: ( card a1) = ((k + 1) - 1) by A41;

        

         A44: (H . A1) on (H . L1) implies A1 on L1

        proof

          (F " (F .: ( ^^ (a1,X,(k + 1))))) c= ( ^^ (a1,X,(k + 1))) & ( ^^ (a1,X,(k + 1))) c= (F " (F .: ( ^^ (a1,X,(k + 1))))) by A21, A36, FUNCT_1: 76, FUNCT_1: 82;

          then

           A45: (F " (F .: ( ^^ (a1,X,(k + 1))))) = ( ^^ (a1,X,(k + 1))) by XBOOLE_0:def 10;

          (H . L1) in the Lines of ( G_ (k,X));

          then

           A46: ex hl1 be Subset of X st hl1 = (H . L1) & ( card hl1) = (k + 1) by A10;

          ( ^^ (a1,X,(k + 1))) is STAR by A11, A43, Th29;

          then (F .: ( ^^ (a1,X,(k + 1)))) is STAR by A3, A4, A13, Th23;

          then

          consider S be Subset of X such that

           A47: ( card S) = ((k + 1) - 1) and

           A48: (F .: ( ^^ (a1,X,(k + 1)))) = { A where A be Subset of X : ( card A) = (k + 1) & S c= A };

          (H . A1) in the Points of ( G_ (k,X));

          then

          consider ha1 be Subset of X such that

           A49: ha1 = (H . A1) and

           A50: ( card ha1) = k by A6;

          reconsider ha1, S as finite Subset of X by A50, A47;

          

           A51: ( ^^ (ha1,X,(k + 1))) = ( ^^ (ha1,X)) by A11, A50, A47, Def13;

          assume (H . A1) on (H . L1);

          then (H . A1) c= (H . L1) by A1, A5, Th10;

          then (F . L11) in ( ^^ (ha1,X,(k + 1))) by A42, A49, A50, A46, A51;

          then L1 in (F " ( ^^ (ha1,X,(k + 1)))) by A36, A42, FUNCT_1:def 7;

          then

           A52: ( meet (F " ( ^^ (ha1,X,(k + 1))))) c= L1 by SETFAM_1: 3;

          ( ^^ (S,X,(k + 1))) = ( ^^ (S,X)) by A11, A47, Def13;

          then

           A53: S = ( meet (F .: ( ^^ (a1,X,(k + 1))))) by A11, A47, A48, Th30;

          ( meet ( ^^ (a1,X,(k + 1)))) = a1 by A11, A41, A47, Th30;

          hence thesis by A1, A5, A40, A38, A49, A50, A48, A51, A53, A52, A45, Th10;

        end;

        

         A54: ( ^^ (a1,X,(k + 1))) = ( ^^ (a1,X)) by A11, A43, Def13;

        A1 on L1 implies (H . A1) on (H . L1)

        proof

          assume A1 on L1;

          then A1 c= L1 by A1, A5, Th10;

          then L1 in ( ^^ (a1,X,(k + 1))) by A40, A41, A39, A54;

          then (F . L11) in (F .: ( ^^ (a1,X,(k + 1)))) by A36, A42, FUNCT_1:def 6;

          then ( meet (F .: ( ^^ (a1,X,(k + 1))))) c= (F . L11) by SETFAM_1: 3;

          hence thesis by A1, A5, A40, A42, A38, Th10;

        end;

        hence thesis by A44;

      end;

      

       A55: ( rng the point-map of F) = the Points of ( G_ ((k + 1),X)) by A21, FUNCT_2:def 3;

      for y be object st y in the Points of ( G_ (k,X)) holds ex x be object st x in the Points of ( G_ (k,X)) & y = (Hp . x)

      proof

        let y be object;

        assume y in the Points of ( G_ (k,X));

        then

         A56: ex Y1 be Subset of X st y = Y1 & ( card Y1) = k by A6;

        then

        reconsider y as finite Subset of X;

        

         A57: ( card y) = ((k + 1) - 1) by A56;

        then ( ^^ (y,X,(k + 1))) is STAR by A11, Th29;

        then (F " ( ^^ (y,X,(k + 1)))) is STAR by A3, A4, A13, Th23;

        then

        consider S be Subset of X such that

         A58: ( card S) = ((k + 1) - 1) and

         A59: (F " ( ^^ (y,X,(k + 1)))) = { A where A be Subset of X : ( card A) = (k + 1) & S c= A };

        

         A60: S in the Points of ( G_ (k,X)) by A6, A58;

        reconsider S as finite Subset of X by A58;

        

         A61: P[S, (Hp . S)] by A9, A60;

        ( ^^ (S,X,(k + 1))) = ( ^^ (S,X)) by A11, A58, Def13;

        then (Hp . S) = ( meet ( ^^ (y,X,(k + 1)))) by A55, A58, A59, A61, FUNCT_1: 77;

        then y = (Hp . S) by A11, A57, Th30;

        hence thesis by A60;

      end;

      then ( rng Hp) = the Points of ( G_ (k,X)) by FUNCT_2: 10;

      then

       A62: Hp is onto by FUNCT_2:def 3;

      

       A63: for A be POINT of ( G_ (k,X)), B be finite set st B = A holds (Hp . A) = ( meet (F .: ( ^^ (B,X,(k + 1)))))

      proof

        let A be POINT of ( G_ (k,X));

        

         A64: P[A, (Hp . A)] by A9;

        let B be finite set;

        assume A = B;

        hence thesis by A64;

      end;

      the line-map of H is bijective by A3, A10, A12;

      hence thesis by A63, A22, A62, A37;

    end;

    theorem :: COMBGRAS:32

    

     Th32: for k be Nat holds for X be non empty set st 0 < k & (k + 3) c= ( card X) holds for F be IncProjMap over ( G_ ((k + 1),X)), ( G_ ((k + 1),X)) st F is automorphism holds for H be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) st the line-map of H = the point-map of F holds for f be Permutation of X st the IncProjMap of H = ( incprojmap (k,f)) holds the IncProjMap of F = ( incprojmap ((k + 1),f))

    proof

      let k be Nat;

      let X be non empty set such that

       A1: 0 < k and

       A2: (k + 3) c= ( card X);

      (k + 1) <= (k + 3) by XREAL_1: 7;

      then ( Segm (k + 1)) c= ( Segm (k + 3)) by NAT_1: 39;

      then

       A3: (k + 1) c= ( card X) by A2;

      then

       A4: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, Def1;

      (k + 2) <= (k + 3) by XREAL_1: 7;

      then ( Segm (k + 2)) c= ( Segm (k + 3)) by NAT_1: 39;

      then

       A5: ((k + 1) + 1) c= ( card X) by A2;

      then

       A6: the Points of ( G_ ((k + 1),X)) = { A where A be Subset of X : ( card A) = (k + 1) } by Def1;

      (k + 0 ) <= (k + 1) by XREAL_1: 7;

      then

       A7: ( Segm k) c= ( Segm (k + 1)) by NAT_1: 39;

      (k + 1) <= (k + 2) by XREAL_1: 7;

      then

       A8: ( Segm (k + 1)) c= ( Segm (k + 2)) by NAT_1: 39;

      let F be IncProjMap over ( G_ ((k + 1),X)), ( G_ ((k + 1),X)) such that

       A9: F is automorphism;

      

       A10: F is incidence_preserving by A9;

      let H be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) such that

       A11: the line-map of H = the point-map of F;

      

       A12: ( dom the point-map of F) = the Points of ( G_ ((k + 1),X)) by FUNCT_2: 52;

      let f be Permutation of X such that

       A13: the IncProjMap of H = ( incprojmap (k,f));

      

       A14: for x be object st x in ( dom the point-map of F) holds (the point-map of F . x) = (the point-map of ( incprojmap ((k + 1),f)) . x)

      proof

        let x be object;

        assume x in ( dom the point-map of F);

        then

        consider A be POINT of ( G_ ((k + 1),X)) such that

         A15: x = A;

        consider A1 be LINE of ( G_ (k,X)) such that

         A16: x = A1 by A4, A6, A15;

        (( incprojmap (k,f)) . A1) = (f .: A1) by A1, A3, Def14;

        then (F . A) = (( incprojmap ((k + 1),f)) . A) by A11, A13, A5, A15, A16, Def14;

        hence thesis by A15;

      end;

      

       A17: the Lines of ( G_ ((k + 1),X)) = { L where L be Subset of X : ( card L) = ((k + 1) + 1) } by A5, Def1;

      

       A18: the point-map of F is bijective by A9;

      

       A19: for x be object st x in ( dom the line-map of F) holds (the line-map of F . x) = (the line-map of ( incprojmap ((k + 1),f)) . x)

      proof

        let x be object;

        assume x in ( dom the line-map of F);

        then

        consider A be LINE of ( G_ ((k + 1),X)) such that

         A20: x = A;

        reconsider x as set by TARSKI: 1;

        x in the Lines of ( G_ ((k + 1),X)) by A20;

        then

         A21: ex A11 be Subset of X st x = A11 & ( card A11) = ((k + 1) + 1) by A17;

        then

        consider B1 be set such that

         A22: B1 c= x and

         A23: ( card B1) = (k + 1) by A8, CARD_FIL: 36;

        

         A24: x is finite by A21;

        then

         A25: ( card (x \ B1)) = ((k + 2) - (k + 1)) by A21, A22, A23, CARD_2: 44;

        B1 c= X by A21, A22, XBOOLE_1: 1;

        then B1 in the Points of ( G_ ((k + 1),X)) by A6, A23;

        then

        consider b1 be POINT of ( G_ ((k + 1),X)) such that

         A26: b1 = B1;

        consider C1 be set such that

         A27: C1 c= B1 and

         A28: ( card C1) = k by A7, A23, CARD_FIL: 36;

        B1 is finite by A23;

        then

         A29: ( card (C1 \/ (x \ B1))) = (k + 1) by A27, A28, A24, A25, CARD_2: 40, XBOOLE_1: 85;

        C1 c= x by A22, A27;

        then

         A30: (C1 \/ (x \ B1)) c= x by XBOOLE_1: 8;

        then (C1 \/ (x \ B1)) c= X by A21, XBOOLE_1: 1;

        then (C1 \/ (x \ B1)) in the Points of ( G_ ((k + 1),X)) by A6, A29;

        then

        consider b2 be POINT of ( G_ ((k + 1),X)) such that

         A31: b2 = (C1 \/ (x \ B1));

        b2 on A by A5, A20, A30, A31, Th10;

        then (F . b2) on (F . A) by A10;

        then

         A32: (F . b2) c= (F . A) by A5, Th10;

        (B1 \/ (C1 \/ (x \ B1))) c= x by A22, A30, XBOOLE_1: 8;

        then

         A33: ( card (b1 \/ b2)) c= (k + 2) by A21, A26, A31, CARD_1: 11;

        B1 misses (x \ B1) by XBOOLE_1: 79;

        then ( card ((x \ B1) /\ B1)) = 0 by CARD_1: 27, XBOOLE_0:def 7;

        then

         A34: b1 <> b2 by A25, A26, A31, XBOOLE_1: 11, XBOOLE_1: 28;

        then ((k + 1) + 1) c= ( card (b1 \/ b2)) by A23, A29, A26, A31, Th1;

        then ( card (b1 \/ b2)) = (k + 2) by A33, XBOOLE_0:def 10;

        then

         A35: (b1 \/ b2) = x by A21, A22, A24, A30, A26, A31, CARD_2: 102, XBOOLE_1: 8;

        (F . b2) in the Points of ( G_ ((k + 1),X));

        then

         A36: ex B12 be Subset of X st (F . b2) = B12 & ( card B12) = (k + 1) by A6;

        (F . b1) in the Points of ( G_ ((k + 1),X));

        then

         A37: ex B11 be Subset of X st (F . b1) = B11 & ( card B11) = (k + 1) by A6;

        (F . A) in the Lines of ( G_ ((k + 1),X));

        then

         A38: ex L1 be Subset of X st (F . A) = L1 & ( card L1) = ((k + 1) + 1) by A17;

        then

         A39: (F . A) is finite;

        (F . b1) <> (F . b2) by A18, A12, A34, FUNCT_1:def 4;

        then

         A40: ((k + 1) + 1) c= ( card ((F . b1) \/ (F . b2))) by A37, A36, Th1;

        b1 on A by A5, A20, A22, A26, Th10;

        then (F . b1) on (F . A) by A10;

        then

         A41: (F . b1) c= (F . A) by A5, Th10;

        then ((F . b1) \/ (F . b2)) c= (F . A) by A32, XBOOLE_1: 8;

        then ( card ((F . b1) \/ (F . b2))) c= (k + 2) by A38, CARD_1: 11;

        then ( card ((F . b1) \/ (F . b2))) = (k + 2) by A40, XBOOLE_0:def 10;

        then

         A42: ((F . b1) \/ (F . b2)) = (F . A) by A41, A32, A38, A39, CARD_2: 102, XBOOLE_1: 8;

        

         A43: (( incprojmap ((k + 1),f)) . A) = (f .: x) by A5, A20, Def14;

        

         A44: ((f .: b1) \/ (f .: b2)) = (f .: (b1 \/ b2)) & (F . b2) = (( incprojmap ((k + 1),f)) . b2) by A12, A14, RELAT_1: 120;

        (F . b1) = (( incprojmap ((k + 1),f)) . b1) & (( incprojmap ((k + 1),f)) . b1) = (f .: b1) by A5, A12, A14, Def14;

        hence thesis by A5, A20, A35, A42, A43, A44, Def14;

      end;

      

       A45: ( dom the line-map of F) = the Lines of ( G_ ((k + 1),X)) & ( dom the line-map of ( incprojmap ((k + 1),f))) = the Lines of ( G_ ((k + 1),X)) by FUNCT_2: 52;

      ( dom the point-map of ( incprojmap ((k + 1),f))) = the Points of ( G_ ((k + 1),X)) by FUNCT_2: 52;

      then the point-map of F = the point-map of ( incprojmap ((k + 1),f)) by A12, A14;

      hence thesis by A45, A19, FUNCT_1:def 11;

    end;

    theorem :: COMBGRAS:33

    

     Th33: for k be Nat holds for X be non empty set st 2 <= k & (k + 2) c= ( card X) holds for F be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) st F is automorphism holds ex s be Permutation of X st the IncProjMap of F = ( incprojmap (k,s))

    proof

      let k be Nat;

      let X be non empty set such that

       A1: 2 <= k and

       A2: (k + 2) c= ( card X);

      defpred P[ Nat] means 1 <= $1 & $1 <= k implies for F be IncProjMap over ( G_ ($1,X)), ( G_ ($1,X)) st F is automorphism holds ex f be Permutation of X st the IncProjMap of F = ( incprojmap ($1,f));

      

       A3: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A4: P[i];

        1 <= (i + 1) & (i + 1) <= k implies for F be IncProjMap over ( G_ ((i + 1),X)), ( G_ ((i + 1),X)) st F is automorphism holds ex f be Permutation of X st the IncProjMap of F = ( incprojmap ((i + 1),f))

        proof

          assume that 1 <= (i + 1) and

           A5: (i + 1) <= k;

          let F2 be IncProjMap over ( G_ ((i + 1),X)), ( G_ ((i + 1),X)) such that

           A6: F2 is automorphism;

          ((i + 1) + 2) <= (k + 2) by A5, XREAL_1: 7;

          then

           A7: ( Segm (i + 3)) c= ( Segm (k + 2)) by NAT_1: 39;

          then

           A8: (i + 3) c= ( card X) by A2;

          

           A9: i = 0 implies ex f be Permutation of X st the IncProjMap of F2 = ( incprojmap ((i + 1),f))

          proof

            (i + 2) <= (i + 3) by XREAL_1: 7;

            then ( Segm (i + 2)) c= ( Segm (i + 3)) by NAT_1: 39;

            then

             A10: ((i + 1) + 1) c= ( card X) by A8;

            assume i = 0 ;

            hence thesis by A6, A10, Th24;

          end;

           0 < i implies ex f be Permutation of X st the IncProjMap of F2 = ( incprojmap ((i + 1),f))

          proof

            assume

             A11: 0 < i;

            then

            consider F1 be IncProjMap over ( G_ (i,X)), ( G_ (i,X)) such that

             A12: F1 is automorphism and

             A13: the line-map of F1 = the point-map of F2 and for A be POINT of ( G_ (i,X)), B be finite set st B = A holds (F1 . A) = ( meet (F2 .: ( ^^ (B,X,(i + 1))))) by A2, A6, A7, Th31, XBOOLE_1: 1;

            ( 0 + 1) < (i + 1) by A11, XREAL_1: 8;

            then

            consider f be Permutation of X such that

             A14: the IncProjMap of F1 = ( incprojmap (i,f)) by A4, A5, A12, NAT_1: 13;

             the IncProjMap of F2 = ( incprojmap ((i + 1),f)) by A2, A6, A7, A11, A13, A14, Th32, XBOOLE_1: 1;

            hence thesis;

          end;

          hence thesis by A9;

        end;

        hence thesis;

      end;

      

       A15: P[ 0 ];

      for i be Nat holds P[i] from NAT_1:sch 2( A15, A3);

      then

       A16: P[k];

      let F be IncProjMap over ( G_ (k,X)), ( G_ (k,X));

      assume F is automorphism;

      hence thesis by A1, A16, XXREAL_0: 2;

    end;

    theorem :: COMBGRAS:34

    

     Th34: for k be Nat holds for X be non empty set st 0 < k & (k + 1) c= ( card X) holds for s be Permutation of X holds ( incprojmap (k,s)) is automorphism

    proof

      let k be Nat;

      let X be non empty set such that

       A1: 0 < k & (k + 1) c= ( card X);

      let s be Permutation of X;

      

       A2: the Points of ( G_ (k,X)) = { A where A be Subset of X : ( card A) = k } by A1, Def1;

      

       A3: the point-map of ( incprojmap (k,s)) is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A4: x1 in ( dom the point-map of ( incprojmap (k,s))) and

         A5: x2 in ( dom the point-map of ( incprojmap (k,s))) and

         A6: (the point-map of ( incprojmap (k,s)) . x1) = (the point-map of ( incprojmap (k,s)) . x2);

        consider X1 be POINT of ( G_ (k,X)) such that

         A7: X1 = x1 by A4;

        x1 in the Points of ( G_ (k,X)) by A4;

        then

         A8: ex X11 be Subset of X st X11 = x1 & ( card X11) = k by A2;

        consider X2 be POINT of ( G_ (k,X)) such that

         A9: X2 = x2 by A5;

        x2 in the Points of ( G_ (k,X)) by A5;

        then

         A10: ex X12 be Subset of X st X12 = x2 & ( card X12) = k by A2;

        

         A11: (( incprojmap (k,s)) . X2) = (s .: X2) by A1, Def14;

        (( incprojmap (k,s)) . X1) = (s .: X1) by A1, Def14;

        hence thesis by A6, A7, A9, A8, A10, A11, Th6;

      end;

      for y be object st y in the Points of ( G_ (k,X)) holds ex x be object st x in the Points of ( G_ (k,X)) & y = (the point-map of ( incprojmap (k,s)) . x)

      proof

        let y be object;

        assume y in the Points of ( G_ (k,X));

        then

         A12: ex B be Subset of X st B = y & ( card B) = k by A2;

        reconsider y as set by TARSKI: 1;

        

         A13: (s " y) c= ( dom s) by RELAT_1: 132;

        then

         A14: (s " y) c= X by FUNCT_2: 52;

        ( rng s) = X by FUNCT_2:def 3;

        then

         A15: (s .: (s " y)) = y by A12, FUNCT_1: 77;

        then ( card (s " y)) = k by A12, A13, Th4;

        then (s " y) in the Points of ( G_ (k,X)) by A2, A14;

        then

        consider A be POINT of ( G_ (k,X)) such that

         A16: A = (s " y);

        y = (( incprojmap (k,s)) . A) by A1, A15, A16, Def14;

        hence thesis;

      end;

      then ( rng the point-map of ( incprojmap (k,s))) = the Points of ( G_ (k,X)) by FUNCT_2: 10;

      then

       A17: the point-map of ( incprojmap (k,s)) is onto by FUNCT_2:def 3;

      

       A18: the Lines of ( G_ (k,X)) = { L where L be Subset of X : ( card L) = (k + 1) } by A1, Def1;

      for y be object st y in the Lines of ( G_ (k,X)) holds ex x be object st x in the Lines of ( G_ (k,X)) & y = (the line-map of ( incprojmap (k,s)) . x)

      proof

        let y be object;

        assume y in the Lines of ( G_ (k,X));

        then

         A19: ex B be Subset of X st B = y & ( card B) = (k + 1) by A18;

        reconsider y as set by TARSKI: 1;

        

         A20: (s " y) c= ( dom s) by RELAT_1: 132;

        then

         A21: (s " y) c= X by FUNCT_2: 52;

        ( rng s) = X by FUNCT_2:def 3;

        then

         A22: (s .: (s " y)) = y by A19, FUNCT_1: 77;

        then ( card (s " y)) = (k + 1) by A19, A20, Th4;

        then (s " y) in the Lines of ( G_ (k,X)) by A18, A21;

        then

        consider A be LINE of ( G_ (k,X)) such that

         A23: A = (s " y);

        y = (( incprojmap (k,s)) . A) by A1, A22, A23, Def14;

        hence thesis;

      end;

      then ( rng the line-map of ( incprojmap (k,s))) = the Lines of ( G_ (k,X)) by FUNCT_2: 10;

      then

       A24: the line-map of ( incprojmap (k,s)) is onto by FUNCT_2:def 3;

      

       A25: ( dom s) = X by FUNCT_2: 52;

      

       A26: ( incprojmap (k,s)) is incidence_preserving

      proof

        let A1 be POINT of ( G_ (k,X));

        let L1 be LINE of ( G_ (k,X));

        

         A27: (s .: A1) = (( incprojmap (k,s)) . A1) & (s .: L1) = (( incprojmap (k,s)) . L1) by A1, Def14;

        A1 in the Points of ( G_ (k,X));

        then

         A28: ex a1 be Subset of X st A1 = a1 & ( card a1) = k by A2;

        

         A29: (( incprojmap (k,s)) . A1) on (( incprojmap (k,s)) . L1) implies A1 on L1

        proof

          assume (( incprojmap (k,s)) . A1) on (( incprojmap (k,s)) . L1);

          then (s .: A1) c= (s .: L1) by A1, A27, Th10;

          then A1 c= L1 by A25, A28, FUNCT_1: 87;

          hence thesis by A1, Th10;

        end;

        A1 on L1 implies (( incprojmap (k,s)) . A1) on (( incprojmap (k,s)) . L1)

        proof

          assume A1 on L1;

          then A1 c= L1 by A1, Th10;

          then (s .: A1) c= (s .: L1) by RELAT_1: 123;

          hence thesis by A1, A27, Th10;

        end;

        hence thesis by A29;

      end;

      the line-map of ( incprojmap (k,s)) is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A30: x1 in ( dom the line-map of ( incprojmap (k,s))) and

         A31: x2 in ( dom the line-map of ( incprojmap (k,s))) and

         A32: (the line-map of ( incprojmap (k,s)) . x1) = (the line-map of ( incprojmap (k,s)) . x2);

        consider X1 be LINE of ( G_ (k,X)) such that

         A33: X1 = x1 by A30;

        x1 in the Lines of ( G_ (k,X)) by A30;

        then

         A34: ex X11 be Subset of X st X11 = x1 & ( card X11) = (k + 1) by A18;

        consider X2 be LINE of ( G_ (k,X)) such that

         A35: X2 = x2 by A31;

        x2 in the Lines of ( G_ (k,X)) by A31;

        then

         A36: ex X12 be Subset of X st X12 = x2 & ( card X12) = (k + 1) by A18;

        

         A37: (( incprojmap (k,s)) . X2) = (s .: X2) by A1, Def14;

        (( incprojmap (k,s)) . X1) = (s .: X1) by A1, Def14;

        hence thesis by A32, A33, A35, A34, A36, A37, Th6;

      end;

      hence thesis by A24, A3, A17, A26;

    end;

    theorem :: COMBGRAS:35

    for X be non empty set st 0 < k & (k + 1) c= ( card X) holds for F be IncProjMap over ( G_ (k,X)), ( G_ (k,X)) holds F is automorphism iff ex s be Permutation of X st the IncProjMap of F = ( incprojmap (k,s))

    proof

      let X be non empty set such that

       A1: 0 < k and

       A2: (k + 1) c= ( card X);

      let F be IncProjMap over ( G_ (k,X)), ( G_ (k,X));

      

       A3: F is automorphism implies ex s be Permutation of X st the IncProjMap of F = ( incprojmap (k,s))

      proof

        

         A4: ( card k) = k & ( succ 1) = (1 + 1);

        

         A5: ( card (k + 1)) = (k + 1);

        (k + 1) in ( succ ( card X)) by A2, ORDINAL1: 22;

        then

         A6: (k + 1) = ( card X) or (k + 1) in ( card X) by ORDINAL1: 8;

        

         A7: ( card 1) = 1;

        ( 0 + 1) < (k + 1) & ( succ ( Segm k)) = ( Segm (k + 1)) by A1, NAT_1: 38, XREAL_1: 8;

        then ( Segm 1) in ( succ ( Segm k)) by A7, A5, NAT_1: 41;

        then 1 = k or ( Segm 1) in ( Segm k) by ORDINAL1: 8;

        then

         A8: 1 = k or 1 < k & ( Segm 2) c= ( Segm k) by A7, A4, NAT_1: 41, ORDINAL1: 21;

        assume

         A9: F is automorphism;

        ( succ ( Segm (k + 1))) = ( Segm ((k + 1) + 1)) by NAT_1: 38;

        then 1 = k or 1 < k & ( card X) = (k + 1) or 2 <= k & (k + 2) c= ( card X) by A6, A8, NAT_1: 39, ORDINAL1: 21;

        hence thesis by A2, A9, Th24, Th25, Th33;

      end;

      (ex s be Permutation of X st the IncProjMap of F = ( incprojmap (k,s))) implies F is automorphism

      proof

        assume ex s be Permutation of X st the IncProjMap of F = ( incprojmap (k,s));

        then

        consider s be Permutation of X such that

         A10: the IncProjMap of F = ( incprojmap (k,s));

        

         A11: ( incprojmap (k,s)) is automorphism by A1, A2, Th34;

        then

         A12: ( incprojmap (k,s)) is incidence_preserving;

        

         A13: F is incidence_preserving

        proof

          let A be POINT of ( G_ (k,X));

          let L be LINE of ( G_ (k,X));

          (F . A) = (( incprojmap (k,s)) . A) & (F . L) = (( incprojmap (k,s)) . L) by A10;

          hence thesis by A12;

        end;

        the line-map of F is bijective & the point-map of F is bijective by A10, A11;

        hence thesis by A13;

      end;

      hence thesis by A3;

    end;