:: Combinatorial {G}rassmannians
:: by Andrzej Owsiejczuk
::
:: Received April 16, 2007
:: Copyright (c) 2007-2026 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;
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;