:: Combinatorial {G}rassmannians :: by Andrzej Owsiejczuk :: :: Received April 16, 2007 :: Copyright (c) 2007-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, INCSP_1, SUBSET_1, CARD_1, XBOOLE_0, ARYTM_3, TARSKI, ORDINAL1, FINSET_1, RELAT_1, ARYTM_1, NAT_1, FUNCT_1, XXREAL_0, FDIFF_1, WELLORD2, ZFMISC_1, ANPROJ_2, AFF_2, MOD_4, FUNCT_2, PRE_POLY, SETFAM_1, COMBGRAS; notations TARSKI, XBOOLE_0, CARD_1, SUBSET_1, ORDINAL1, ENUMSET1, ZFMISC_1, SETFAM_1, DOMAIN_1, FINSET_1, RELAT_1, RELSET_1, WELLORD2, NUMBERS, INCSP_1, XXREAL_0, XCMPLX_0, REAL_1, FUNCT_1, FUNCT_2, INCPROJ, NAT_1; constructors SETFAM_1, WELLORD2, DOMAIN_1, REAL_1, NAT_1, BINOP_2, INCPROJ, RELSET_1, XREAL_0, INT_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, XREAL_0, NAT_1, CARD_1, INCSP_1, RELSET_1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; definitions TARSKI, INCSP_1, INCPROJ, FUNCT_1; equalities RELAT_1, ORDINAL1, CARD_1; expansions TARSKI, INCSP_1, INCPROJ, FUNCT_1; theorems ENUMSET1, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, XREAL_1, SETFAM_1, PENCIL_1, INCSP_1, WELLORD2, CARD_1, CARD_2, NAT_1, ORDINAL1, CARD_FIL, STIRL2_1, XXREAL_0, FUNCT_1, FUNCT_2, RELAT_1, RELSET_1; schemes FUNCT_1, NAT_1, CLASSES1; begin :: Preliminaries reserve k,n for Nat, x,y,X,Y,Z for set; theorem Th1: for a,b being 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,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 Th2: for a,b being 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 Th3: card X c= card Y iff ex f being 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 being 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 being 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 being 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 being 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 Th4: for f being 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 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,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,81; then Z c= Y by XBOOLE_1:37; hence thesis by A5,XBOOLE_0:def 10; end; theorem Th6: for Y being non empty set for p being Function of X,Y st p is one-to-one for x1,x2 being 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 being 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 being 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 being 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 being 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 Th7: for a,b,c being 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 being 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 being 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 being object such that A12: {x3} = c \ (a /\ c) by CARD_2:42; A13: a = (a /\ b) \/ {x1} by A10,XBOOLE_1:17,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,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,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 being 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,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,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 being 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 being 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,86; then A48: a /\ c = a \ {x1} by A5,A44,CARD_2:102; a /\ b c= a \ {x1} by A46,XBOOLE_1:17,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 being 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 for P1,P2 being IncProjStr st the IncProjStr of P1 = the IncProjStr of P2 for A1 being POINT of P1, A2 being POINT of P2 st A1 = A2 for L1 being LINE of P1, L2 being LINE of P2 st L1 = L2 holds A1 on L1 implies A2 on L2; theorem Th9: for P1,P2 being IncProjStr st the IncProjStr of P1 = the IncProjStr of P2 for A1 being Subset of the Points of P1 for A2 being Subset of the Points of P2 st A1 = A2 for L1 being LINE of P1, L2 being 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 being 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 being LINE of IT ex A,B being 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 being 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 being 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 being POINT of IT, K,L being 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 :: Configuration G definition mode PartialLinearSpace is with_non-trivial_lines up-2-rank IncProjStr; end; definition let k be Nat; let X be non empty set such that A1: 0 < k and A2: k + 1 c= card X; func G_(k,X) -> strict PartialLinearSpace means :Def1: the Points of it = {A where A is Subset of X: card A = k} & the Lines of it = {L where L is 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 is Subset of X: card B = k + 1}; set P = {A where A is Subset of X: card A = k}; set I = (RelIncl bool X) /\ [:P,L:]; consider B being 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 being 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 being POINT of G; let l1,l2 being 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 being Subset of X st b = B & card B = k; a in P; then A10: ex A being 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 being 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 being 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 being LINE of G; l in L; then consider C being 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 being 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 Th10: for k being Nat for X being non empty set st 0 < k & k + 1 c= card X for A being POINT of G_(k,X) for L being 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 is 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 being Subset of X st A1 = A & card A1 = k by A2; A4: the Lines of G_(k,X) = {L where L is 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 being 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 Th11: for k being Element of NAT for X being 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 is 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 is 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 being 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 being Subset of X st K2 = L2 & card K2 = k + 1 by A17; A3 in the Points of G_(k,X); then A21: ex B3 being Subset of X st B3 = A3 & card B3 = k by A3; A1 in the Points of G_(k,X); then ex B1 being 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 being 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 being Subset of X st B4 = A4 & card B4 = k by A3; A2 in the Points of G_(k,X); then ex B2 being 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 being 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 being 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 being 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 Th12: for k being Element of NAT for X being non empty set st 0 < k & k + 1 c= card X holds for A1,A2,A3,A4,A5,A6 being POINT of G_(k,X) for L1,L2,L3 ,L4 being 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 being 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 is Subset of X: card A = k} by A1,A2 ,Def1; A4: the Lines of G_(k,X) = {L where L is 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 being Subset of X st B5 = A5 & card B5 = k by A3; A2 in the Points of G_(k,X); then A23: ex B2 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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,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 being 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,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 being 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,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 being 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,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 being 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 being 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,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,27; end; hence thesis by A30,A31,A49; end; theorem for k being Element of NAT for X being 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 is 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 being 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 being 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 being 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,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 being 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 is Subset of X: card A = k} by A1,A2 ,Def1; o in the Points of G_(k,X); then A80: ex o1 being Subset of X st o1 = o & card o1 = k by A79; b1 in the Points of G_(k,X); then A81: ex b11 being Subset of X st b11 = b1 & card b11 = k by A79; a3 in the Points of G_(k,X); then A82: ex a13 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being object such that A106: o = {z1} by A80,CARD_2:42; consider z3 being object such that A107: b1 = {z3} by A81,A105,CARD_2:42; consider z2 being 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 being 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 being 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 being 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 being 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 being 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 being LINE of G_(k,X) st {r,s,t} on O proof A128: card(r \/ s \/ t) = k + 1 implies ex O being 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 being 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 being 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; attr K is clique means for A,B being POINT of S st A in K & B in K ex L being LINE of S st {A,B} on L; end; definition let S be IncProjStr; let K be Subset of the Points of S; attr K is maximal_clique means K is clique & for U being 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); attr T is STAR means ex S being Subset of X st card S = k - 1 & T = { A where A is Subset of X: card A = k & S c= A}; attr T is TOP means ex S being Subset of X st card S = k + 1 & T = {A where A is Subset of X: card A = k & A c= S}; end; theorem Th14: for k being Element of NAT for X being non empty set st 2 <= k & k + 2 c= card X for K being 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 is Subset of X: card A = k} by A1,Def1; A8: the Lines of G_(k,X) = {L where L is 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 being Subset of X such that A11: card S = k - 1 and A12: K = {A where A is 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 being 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 being object such that A19: A in U and A20: not A in K; reconsider A as set by TARSKI:1; consider A2 being 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 being 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 being 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 being 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 being 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 being LINE of G_(k,X) st {A2,B} on L; then consider L being 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 being 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 being 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 being 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,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 being LINE of G_(k,X) st {A2,B} on L proof assume ex L being LINE of G_(k,X) st {A2,B} on L; then consider L being 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 being 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,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 being Subset of X st A1 = A & card A1 = k & S c= A1 by A12,A58; then A61: A is finite; A62: ex B1 being 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 being 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 being 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 being 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 being 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 being 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 being Subset of X such that A77: card S = k + 1 and A78: K = {A where A is Subset of X: card A = k & A c= S}; reconsider S as finite set by A77; A79: for U being 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 being object such that A84: A in U and A85: not A in K; reconsider A as set by TARSKI:1; consider A2 being 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 being 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 being 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,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 being 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 being 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 being 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 being 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 being LINE of G_(k,X) st {A2,B} on L proof assume ex L being LINE of G_(k,X) st {A2,B} on L; then consider L being 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 being 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 being LINE of G_(k,X) such that A126: L = S; ex B1 being 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 being 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 Th15: for k being Element of NAT for X being non empty set st 2 <= k & k + 2 c= card X for K being 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 is 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 is 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 being 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 being 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 being 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 being LINE of G_(k,X) such that A23: L = A \/ {x}; consider U being 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 being object such that A31: K = {A3} by CARD_2:42; A32: A3 in K by A31,TARSKI:def 1; then consider A being POINT of G_(k,X) such that A33: A = A3; A3 in the Points of G_(k,X) by A32; then A34: ex A4 being 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 being 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 being 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 being 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 being 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 being 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 being set such that A55: R c= K and A56: card R = 2 by CARD_FIL:36; consider A1,B1 being 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 being 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 being POINT of G_(k,X) such that A64: B = B1; consider L being 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 being 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 being Subset of X st B2 = B & card B2 = k by A7,A63,A64; then A75: B is finite; A76: ex A2 being 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 being 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 being 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 being 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 being 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 being object such that A90: B \ (A /\ B) = {z2} by CARD_2:42; A91: B = (A /\ B) \/ {z2} by A90,XBOOLE_1:17,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 being 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 being 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 being 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 being 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 being Subset of X such that A119: E1 = E2 and A120: card E1 = k by A7; consider E being POINT of G_(k,X) such that A121: E = E1 by A112,A119; A122: A = (A /\ B) \/ {z1} by A89,XBOOLE_1:17,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 being set such that A126: S = {D where D is Subset of X: card D = k & A /\ B c= D}; A127: E2 in K by A112,XBOOLE_0:def 5; then consider K1 being LINE of G_(k,X) such that A128: {A,E} on K1 by A13,A55,A59,A61,A119,A121; consider K2 being 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 being 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 being 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 being 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 being object such that A144: E \ (A /\ B) = {z4} by CARD_2:42; A145: E = (A /\ B) \/ {z4} by A142,A144,XBOOLE_1:17,45; A146: K c= S proof assume not K c= S; then consider D2 being 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 being Subset of X such that A149: D1 = D2 and A150: card D1 = k by A7; consider D being POINT of G_(k,X) such that A151: D = D1 by A147,A149; consider K11 being 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 being Subset of X st R11 = K11 & card R11 = k + 1 by A14; A155: card D = (k - 1) + 1 by A150,A151; consider K13 being LINE of G_(k,X) such that A156: {E,D} on K13 by A13,A127,A119,A121,A147,A149,A151; consider K12 being 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 being 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 being 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 being 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,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,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 being 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,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 being Subset of X st Z = Z1 & card Z1 = k & A /\ B c= Z1 by A126; hence thesis by A7; end; then consider S1 being 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 being 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 being POINT of G_(k,X) st C in K & C on L & A <> C & B <> C; then consider C being 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 being 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 being set such that A198: T = {D where D is 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 being Subset of X such that A203: D1 = D2 and A204: card D1 = k by A7; consider D being 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 being 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 being 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 being 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 being LINE of G_(k,X) such that A221: {B,D} on L12 by A13,A55,A62,A64,A201,A203,A205; consider L11 being 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 being 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 being 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 being Subset of X st e = E & card E = k & E c= L by A198; hence thesis by A7; end; then consider T1 being 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 :: Automorphisms definition let S1,S2 be IncProjStr; struct IncProjMap over S1,S2 (#point-map -> Function of the Points of S1, the Points of S2, line-map -> Function of the Lines of S1, the Lines of S2#); end; definition let S1,S2 be IncProjStr; let F be IncProjMap over S1,S2; let a be POINT of S1; 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; func F.L -> LINE of S2 equals (the line-map of F).L; coherence; end; theorem Th16: for S1,S2 being IncProjStr for F1,F2 being IncProjMap over S1,S2 st (for A being POINT of S1 holds F1.A = F2.A) & (for L being 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 being POINT of S1 holds F1.A = F2.A and A2: for L being LINE of S1 holds F1.L = F2.L; for a being 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 being 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 being 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 being 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; attr F is incidence_preserving means for A1 being POINT of S1 for L1 being LINE of S1 holds (A1 on L1 iff F.A1 on F.L1); end; theorem for S1,S2 being IncProjStr for F1,F2 being 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; 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; 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 being 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; 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; func ^^(A,X) -> Subset of bool X equals {B where B is Subset of X: card B = (card A)+1 & A c= B}; coherence proof set Y = {B where B is 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 being 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 such that A1: 0 < k & k + 1 c= card X; let A be finite set such that A2: card A = k - 1; 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 is 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 being 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 Th18: for S1,S2 being IncProjStr for F being IncProjMap over S1,S2 for K being Subset of the Points of S1 holds F.:K = {B where B is POINT of S2:ex A being 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 is POINT of S2:ex A being 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 being 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 being 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 being 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 being POINT of S2 st B = b & ex A being 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 for S1,S2 being IncProjStr for F being IncProjMap over S1,S2 for K being Subset of the Points of S2 holds F"K = {A where A is POINT of S1:ex B being 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 is POINT of S1:ex B being 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 being 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 being 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 being POINT of S1 st A = a & ex B being 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 Th20: for S being IncProjStr for F being IncProjMap over S,S for K being 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 is POINT of S:ex A being POINT of S st (A in K & F.A = B)} by Th18; then consider B11 being POINT of S such that A6: B1 = B11 and A7: ex A being POINT of S st A in K & F.A = B11 by A3; consider B12 being POINT of S such that A8: B2 = B12 and A9: ex A being POINT of S st A in K & F.A = B12 by A5,A4; consider A12 being POINT of S such that A10: A12 in K and A11: F.A12 = B12 by A9; consider A11 being POINT of S such that A12: A11 in K and A13: F.A11 = B11 by A7; consider L1 being 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 Th21: for S being IncProjStr for F being IncProjMap over S,S for K being 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 being 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 being 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 being 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 Th22: for S being IncProjStr for F being IncProjMap over S,S for K being 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 being 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 being 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 Th23: for k being Element of NAT for X being non empty set st 2 <= k & k + 2 c= card X for F being IncProjMap over G_(k,X), G_(k,X) st F is automorphism for K being 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 is Subset of X: card A = k} by A1,Def1; A14: the Lines of G_(k,X) = {L where L is 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 being Subset of X such that A18: card B = k + 1 & F"K = {A where A is Subset of X: card A = k & A c= B}; consider X1 being 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 being set such that A22: X2 c= B \ X1 and A23: card X2 = 1 by A8,CARD_FIL:36; consider m being 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 being 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 being 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 being 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 being 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 being POINT of G_(k,X) such that A33: B \ X1 = B1; consider S being Subset of X such that A34: card S = k - 1 and A35: K = {A where A is Subset of X: card A = k & S c= A} by A9; consider A1 being 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,106; hence contradiction by A23,A28; end; consider A3 being 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 being 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 being Subset of X st A1 = A11 & card A11 = k & S c= A11 by A35; then A46: card A1 = (k - 1) + 1; consider A2 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being Subset of X such that A86: card B = k + 1 & F.:K = {A where A is Subset of X: card A = k & A c= B}; B in the Lines of G_(k,X) by A14,A86; then consider L2 being 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 being 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 being LINE of G_(k,X) such that A90: l1 = L1 by A88; A91: L2 = F.L1 by A89,A90; consider X1 being 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 being set such that A95: X2 c= B \ X1 and A96: card X2 = 1 by A8,CARD_FIL:36; consider m being 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 being 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 being POINT of G_(k,X) such that A102: B \ X3 = B3; L1 in the Lines of G_(k,X); then A103: ex l12 being 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 being 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 being Subset of X such that A107: card S = k - 1 and A108: K = {A where A is 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 being 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 being POINT of G_(k,X) such that A116: a3 = A3 by A114; consider a1 being 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 being POINT of G_(k,X) such that A119: a1 = A1 by A117; B3 in F.:K by A86,A101,A110,A102; then ex C3 being 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 being 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 being 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 being 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,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 being 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 being 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 being POINT of G_(k,X) such that A139: a2 = A2 by A137; B2 in F.:K by A86,A133,A135,A134; then ex C2 being 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 being 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 being 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 being 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 being 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 such that A1: 0 < k & k + 1 c= card X; let s be Permutation of X; func incprojmap(k,s) -> strict IncProjMap over G_(k,X), G_(k,X) means :Def14 : (for A being POINT of G_(k,X) holds it.A = s.:A) & for L being LINE of G_(k,X ) holds it.L = s.:L; existence proof deffunc F(set) = s.:\$1; consider P being 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 is 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 being 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 being 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 being 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 is Subset of X: card L = k + 1} by A1 ,Def1; consider L being 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 being 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 being 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 being 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 being POINT of G_(k,X) holds f1.A = s.:A and A19: for L being LINE of G_(k,X) holds f1.L = s.:L and A20: for A being POINT of G_(k,X) holds f2.A = s.:A and A21: for L being LINE of G_(k,X) holds f2.L = s.:L; A22: for L being 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 being 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 Th24: for k being Nat for X being non empty set st k = 1 & k + 1 c= card X for F being IncProjMap over G_(k,X), G_(k,X) st F is automorphism holds ex s being 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 is Subset of X: card A = 1} by A1,Def1; consider c being Function such that A3: dom c = X and A4: for x being 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 being 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 being Function such that A10: dom f = X and A11: for x being 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 being 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 being POINT of G_(k,X) such that A15: A = F.(c.a); A in the Points of G_(k,X); then A16: ex A1 being Subset of X st A1 = A & card A1 = 1 by A2; then consider x being 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 being POINT of G_(k,X) such that A23: A1 = F.(c.x1); A1 in the Points of G_(k,X); then ex A11 being Subset of X st A11 = A1 & card A11 = 1 by A2; then consider y1 being object such that A24: A1 = {y1} by CARD_2:42; A25: c.x1 = {x1} & c.x2 = {x2} by A4; consider A2 being POINT of G_(k,X) such that A26: A2 = F.(c.x2); A2 in the Points of G_(k,X); then ex A12 being Subset of X st A12 = A2 & card A12 = 1 by A2; then consider y2 being 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 being object st y in X ex x being 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 being 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 being Subset of X st A1 = a & card A1 = 1 by A2; then consider x being 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 is Subset of X: card L = 1 + 1} by A1 ,Def1; A37: for x being 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 being LINE of G_(k,X) such that A39: x = A; consider A11 being Subset of X such that A40: x = A11 and A41: card A11 = 2 by A36,A35,A38; consider x1,x2 being 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 being POINT of G_(k,X) such that A44: A1 = {x1}; c.x2 = {x2} by A4; then consider A2 being 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 being Subset of X st B2 = F.A2 & card B2 = 1 by A2; then consider y2 being 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 being Subset of X st B1 = F.A1 & card B1 = 1 by A2; then A53: ex y1 being 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 being 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 being 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 being POINT of G_(k,X) such that A64: x = A; A65: ex A1 being Subset of X st x = A1 & card A1 = 1 by A2,A19,A63; then consider x1 being 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 being Subset of X such that A68: B = F.A and A69: card B = 1 by A2; A70: ex x2 being 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 Th25: for k being Nat for X being non empty set st 1 < k & card X = k + 1 for F being IncProjMap over G_(k,X), G_(k,X) st F is automorphism holds ex s being 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 being Function such that A3: dom c = X and A4: for x being 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 is 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 being 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 being Function such that A13: dom f = X and A14: for x being 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 being 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 being POINT of G_(k,X) such that A18: A = F.(c.a); A in the Points of G_(k,X); then ex A1 being 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 being 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 being POINT of G_(k,X) such that A24: A1 = F.(c.x1); consider A2 being POINT of G_(k,X) such that A25: A2 = F.(c.x2); A2 in the Points of G_(k,X); then A26: ex A12 being 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 being object such that A27: X \ A2 = {y2} by CARD_2:42; A1 in the Points of G_(k,X); then A28: ex A11 being 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 being 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 being object st y in X ex x being 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 being 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 being 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 being 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 being 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 being POINT of G_(k,X) such that A43: x = A; F.A in the Points of G_(k,X); then A44: ex B being 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 being 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,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 being 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,48; card(X \ A) = (k + 1) - k by A2,A5,A43,A48,CARD_2:44; then consider x1 being 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 is Subset of X: card L = k + 1} by A1,A2 ,Def1; A54: for x being 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 being LINE of G_(k,X) such that A56: x = A; F.A in the Lines of G_(k,X); then ex y being 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 being 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 Th26: for k being Element of NAT for X being non empty set st 0 < k & k + 1 c= card X for T being Subset of the Points of G_(k,X) for S being Subset of X holds card S = k - 1 & T = {A where A is 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 is 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 being 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,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 being object such that A11: a1 in T by A6,XBOOLE_0:def 1; reconsider a1 as set by TARSKI:1; A12: ex A1 being 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 being 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 being 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 being set st a1 in T holds S c= a1 proof let a1 be set; assume a1 in T; then ex A1 being 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 ::LemStarb: for k being Element of NAT for X being non empty set st 0 < k & k + 1 c= card X for T being Subset of the Points of G_(k,X) st T is STAR for S being Subset of X holds S = meet T implies card S = k - 1 & T = {A where A is 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 being Subset of X such that A2: card S1 = k - 1 & T = {A where A is 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 Th28: for k being Element of NAT for X being non empty set st 0 < k & k + 1 c= card X for T1,T2 being 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 being Subset of X such that A5: card S2 = k - 1 & T2 = {A where A is Subset of X: card A = k & S2 c= A} by A3; A6: S2 = meet T2 by A1,A5,Th26; consider S1 being Subset of X such that A7: card S1 = k - 1 & T1 = {A where A is 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 Th29: for k being Element of NAT for X being non empty set st k + 1 c= card X for A being 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 Th30: for k being Element of NAT for X being non empty set st k + 1 c= card X for A being 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 Th31: for k being Nat for X being non empty set st 0 < k & k + 3 c= card X for F being IncProjMap over G_(k+1,X), G_(k+1,X) st F is automorphism ex H being IncProjMap over G_(k,X), G_(k,X) st H is automorphism & the line-map of H = the point-map of F & for A being POINT of G_(k,X), B being 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 being 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 is Subset of X: card A = k} by A1,Def1; A7: for e being object st e in the Points of G_(k,X) ex u being object st P[e,u] proof let e be object; assume e in the Points of G_(k,X); then ex B being 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 being Function such that A8: dom Hp = the Points of G_(k,X) and A9: for e being 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 is 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 is 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 being object such that A14: x in dom Hp and A15: y = Hp.x by FUNCT_1:def 3; consider B being finite set such that A16: B = x and A17: y = meet(F.:(^^(B,X,k+1))) by A8,A9,A14,A15; A18: ex x1 being 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 being Subset of X such that A19: card S = (k+1) - 1 and A20: F.:(^^(B,X,k+1)) = {C where C is 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 being finite set such that A26: X2 = x2 and A27: Hp.x2 = meet(F.:(^^(X2,X,k+1))) by A9,A24; A28: ex x12 being 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 being finite set such that A32: X1 = x1 and A33: Hp.x1 = meet(F.:(^^(X1,X,k+1))) by A9,A23; A34: ex x11 being 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 being Subset of X st l1 = L1 & card l1 = k+1 by A10; A1 in the Points of G_(k,X); then consider a1 being Subset of X such that A40: a1 = A1 and A41: card a1 = k by A6; consider L11 being 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,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 being 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 being Subset of X such that A47: card S = (k+1) - 1 and A48: F.:(^^(a1,X,k+1)) = {A where A is Subset of X: card A = k+1 & S c= A}; H.A1 in the Points of G_(k,X); then consider ha1 being 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 being object st y in the Points of G_(k,X) ex x being 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 being 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 being Subset of X such that A58: card S = (k+1) - 1 and A59: F"(^^(y,X,k+1)) = {A where A is 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 being POINT of G_(k,X), B being 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 Th32: for k being Nat for X being non empty set st 0 < k & k + 3 c= card X for F being IncProjMap over G_(k+1,X), G_(k+1,X) st F is automorphism for H being IncProjMap over G_(k,X), G_(k,X) st the line-map of H = the point-map of F for f being 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 is 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 is 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 being 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 being POINT of G_(k+1,X) such that A15: x = A; consider A1 being 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 is Subset of X: card L = (k + 1) + 1} by A5,Def1; A18: the point-map of F is bijective by A9; A19: for x being 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 being 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 being Subset of X st x = A11 & card A11 = (k + 1) + 1 by A17; then consider B1 being 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 being POINT of G_(k+1,X) such that A26: b1 = B1; consider C1 being 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 being 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,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 being 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 being 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 being 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 Th33: for k being Nat for X being non empty set st 2 <= k & k + 2 c= card X for F being IncProjMap over G_(k,X), G_(k,X) st F is automorphism holds ex s being 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 being IncProjMap over G_(\$1,X), G_(\$1,X) st F is automorphism ex f being Permutation of X st the IncProjMap of F = incprojmap(\$1,f); A3: for i being 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 being IncProjMap over G_(i+1,X), G_(i+1,X) st F is automorphism ex f being 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 being 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 being Permutation of X st the IncProjMap of F2 = incprojmap(i+1,f) proof assume A11: 0 < i; then consider F1 being 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 being POINT of G_(i,X), B being 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 being 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 being 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 Th34: for k being Nat for X being non empty set st 0 < k & k + 1 c= card X for s being 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 is 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 being 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 being Subset of X st X11 = x1 & card X11 = k by A2; consider X2 being 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 being 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 being object st y in the Points of G_(k,X) ex x being 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 being 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 being 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 is Subset of X: card L = k + 1} by A1 ,Def1; for y being object st y in the Lines of G_(k,X) ex x being 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 being 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 being 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 being 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 being 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 being Subset of X st X11 = x1 & card X11 = k + 1 by A18; consider X2 being 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 being 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 for X being non empty set st 0 < k & k + 1 c= card X for F being IncProjMap over G_(k,X), G_(k,X) holds F is automorphism iff ex s being 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 being 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 being Permutation of X st the IncProjMap of F = incprojmap(k,s)) implies F is automorphism proof assume ex s being Permutation of X st the IncProjMap of F = incprojmap(k ,s); then consider s being 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;