let d' be Element of NAT ; :: thesis:
let d be non zero Element of NAT ; :: thesis:
let G be Grating of d; :: thesis:
assume A1: d = d' + 1 ; :: thesis:
then A2: d' < d by NAT_1:13;
let A be Cell of d',G; :: thesis:
consider l, r being Element of REAL d, i0 being Element of Seg d such that
A3: ( A = cell l,r & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) by A1, Th42;

A4: now

let i be Element of Seg d; :: thesis:
( i = i0 or i <> i0 ) ;
hence l . i <= r . i by A3; :: thesis:

end;

ex B1, B2 being set st
( B1 in star A & B2 in star A & B1 <> B2 & ( for B being set holds
( not B in star A or B = B1 or B = B2 ) ) )

proof

ex l1, r1 being Element of REAL d st
( [(l1 . i0),(r1 . i0)] is Gap of G . i0 & r1 . i0 = l . i0 & ( ( l1 . i0 < r1 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l1 . i = l . i & r1 . i = r . i ) ) ) or for i being Element of Seg d holds
( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) ) )

proof

consider l1i0 being Real such that
A5: [l1i0,(l . i0)] is Gap of G . i0 by A3, Th20;

per cases by A5, Th17;

suppose A6: l1i0 < l . i0 ; :: thesis:

defpred S₁[ Element of Seg d, Real] means ( ( $1 = i0 implies $2 = l1i0 ) & ( $1 <> i0 implies $2 = l . $1 ) );
A7: for i being Element of Seg d ex li being Real st S₁[i,li]

proof

let i be Element of Seg d; :: thesis:
( i = i0 or i <> i0 ) ;
hence ex li being Real st S₁[i,li] ; :: thesis:

end;

consider l1 being Function of (Seg d),REAL such that
A8: for i being Element of Seg d holds S₁[i,l1 . i] from FUNCT_2:sch 3(A7);
reconsider l1 = l1 as Element of REAL d by Def4;
take l1 ; :: thesis:
take r ; :: thesis:
thus ( [(l1 . i0),(r . i0)] is Gap of G . i0 & r . i0 = l . i0 & ( ( l1 . i0 < r . i0 & ( for i being Element of Seg d st i <> i0 holds
( l1 . i = l . i & r . i = r . i ) ) ) or for i being Element of Seg d holds
( r . i < l1 . i & [(l1 . i),(r . i)] is Gap of G . i ) ) ) by A3, A5, A6, A8; :: thesis:

end;

suppose A9: l . i0 < l1i0 ; :: thesis:

consider l1, r1 being Element of REAL d such that
A10: ( cell l1,r1 = infinite-cell G & ( for i being Element of Seg d holds
( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) ) ) by Def11;
take l1 ; :: thesis:
take r1 ; :: thesis:
( r1 . i0 < l1 . i0 & [(l1 . i0),(r1 . i0)] is Gap of G . i0 ) by A10;
hence ( [(l1 . i0),(r1 . i0)] is Gap of G . i0 & r1 . i0 = l . i0 & ( ( l1 . i0 < r1 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l1 . i = l . i & r1 . i = r . i ) ) ) or for i being Element of Seg d holds
( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) ) ) by A5, A9, A10, Th23; :: thesis:

end;

then consider l1, r1 being Element of REAL d such that
A11: ( [(l1 . i0),(r1 . i0)] is Gap of G . i0 & r1 . i0 = l . i0 & ( ( l1 . i0 < r1 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l1 . i = l . i & r1 . i = r . i ) ) ) or for i being Element of Seg d holds
( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) ) ) ;

A12: now

let i be Element of Seg d; :: thesis:
A13: ( i <> i0 & l1 . i = l . i & r1 . i = r . i implies [(l1 . i),(r1 . i)] is Gap of G . i ) by A3;
( i = i0 or i <> i0 ) ;
hence [(l1 . i),(r1 . i)] is Gap of G . i by A11, A13; :: thesis:

end;

A14: ( for i being Element of Seg d holds l1 . i < r1 . i or for i being Element of Seg d holds r1 . i < l1 . i )

proof

per cases by A11;

suppose A15: ( l1 . i0 < r1 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l1 . i = l . i & r1 . i = r . i ) ) ) ; :: thesis:

now

let i be Element of Seg d; :: thesis:
A16: ( i <> i0 & l1 . i = l . i & r1 . i = r . i implies l1 . i < r1 . i ) by A3;
( i = i0 or i <> i0 ) ;
hence l1 . i < r1 . i by A15, A16; :: thesis:

end;

hence ( for i being Element of Seg d holds l1 . i < r1 . i or for i being Element of Seg d holds r1 . i < l1 . i ) ; :: thesis:

end;

suppose for i being Element of Seg d holds
( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) ; :: thesis:

hence ( for i being Element of Seg d holds l1 . i < r1 . i or for i being Element of Seg d holds r1 . i < l1 . i ) ; :: thesis:

end;

then reconsider B1 = cell l1,r1 as Cell of d,G by A12, Th41;
ex l2, r2 being Element of REAL d st
( [(l2 . i0),(r2 . i0)] is Gap of G . i0 & l2 . i0 = l . i0 & ( ( l2 . i0 < r2 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l2 . i = l . i & r2 . i = r . i ) ) ) or for i being Element of Seg d holds
( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) ) )

proof

consider r2i0 being Real such that
A17: [(l . i0),r2i0] is Gap of G . i0 by A3, Th19;

per cases by A17, Th17;

suppose A18: l . i0 < r2i0 ; :: thesis:

defpred S₁[ Element of Seg d, Real] means ( ( $1 = i0 implies $2 = r2i0 ) & ( $1 <> i0 implies $2 = r . $1 ) );
A19: for i being Element of Seg d ex ri being Real st S₁[i,ri]

proof

let i be Element of Seg d; :: thesis:
( i = i0 or i <> i0 ) ;
hence ex ri being Real st S₁[i,ri] ; :: thesis:

end;

consider r2 being Function of (Seg d),REAL such that
A20: for i being Element of Seg d holds S₁[i,r2 . i] from FUNCT_2:sch 3(A19);
reconsider r2 = r2 as Element of REAL d by Def4;
take l ; :: thesis:
take r2 ; :: thesis:
thus ( [(l . i0),(r2 . i0)] is Gap of G . i0 & l . i0 = l . i0 & ( ( l . i0 < r2 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = l . i & r2 . i = r . i ) ) ) or for i being Element of Seg d holds
( r2 . i < l . i & [(l . i),(r2 . i)] is Gap of G . i ) ) ) by A17, A18, A20; :: thesis:

end;

suppose A21: r2i0 < l . i0 ; :: thesis:

consider l2, r2 being Element of REAL d such that
A22: ( cell l2,r2 = infinite-cell G & ( for i being Element of Seg d holds
( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) ) ) by Def11;
take l2 ; :: thesis:
take r2 ; :: thesis:
( r2 . i0 < l2 . i0 & [(l2 . i0),(r2 . i0)] is Gap of G . i0 ) by A22;
hence ( [(l2 . i0),(r2 . i0)] is Gap of G . i0 & l2 . i0 = l . i0 & ( ( l2 . i0 < r2 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l2 . i = l . i & r2 . i = r . i ) ) ) or for i being Element of Seg d holds
( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) ) ) by A17, A21, A22, Th23; :: thesis:

end;

then consider l2, r2 being Element of REAL d such that
A23: ( [(l2 . i0),(r2 . i0)] is Gap of G . i0 & l2 . i0 = l . i0 & ( ( l2 . i0 < r2 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l2 . i = l . i & r2 . i = r . i ) ) ) or for i being Element of Seg d holds
( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) ) ) ;

A24: now

let i be Element of Seg d; :: thesis:
A25: ( i <> i0 & l2 . i = l . i & r2 . i = r . i implies [(l2 . i),(r2 . i)] is Gap of G . i ) by A3;
( i = i0 or i <> i0 ) ;
hence [(l2 . i),(r2 . i)] is Gap of G . i by A23, A25; :: thesis:

end;

( for i being Element of Seg d holds l2 . i < r2 . i or for i being Element of Seg d holds r2 . i < l2 . i )

proof

per cases by A23;

suppose A26: ( l2 . i0 < r2 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l2 . i = l . i & r2 . i = r . i ) ) ) ; :: thesis:

now

let i be Element of Seg d; :: thesis:
A27: ( i <> i0 & l2 . i = l . i & r2 . i = r . i implies l2 . i < r2 . i ) by A3;
( i = i0 or i <> i0 ) ;
hence l2 . i < r2 . i by A26, A27; :: thesis:

end;

hence ( for i being Element of Seg d holds l2 . i < r2 . i or for i being Element of Seg d holds r2 . i < l2 . i ) ; :: thesis:

end;

suppose for i being Element of Seg d holds
( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) ; :: thesis:

hence ( for i being Element of Seg d holds l2 . i < r2 . i or for i being Element of Seg d holds r2 . i < l2 . i ) ; :: thesis:

end;

then reconsider B2 = cell l2,r2 as Cell of d,G by A24, Th41;
take B1 ; :: thesis:
take B2 ; :: thesis:
A c= B1

proof

per cases by A11;

suppose A28: ( l1 . i0 < r1 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l1 . i = l . i & r1 . i = r . i ) ) ) ; :: thesis:

A29: now

let i be Element of Seg d; :: thesis:
( i = i0 or ( i <> i0 & l1 . i = l . i & r1 . i = r . i ) ) by A28;
hence l1 . i <= r1 . i by A3, A28; :: thesis:

end;

now

let i be Element of Seg d; :: thesis:
( i = i0 or ( i <> i0 & l1 . i = l . i & r1 . i = r . i ) ) by A28;
hence ( l1 . i <= l . i & l . i <= r . i & r . i <= r1 . i ) by A3, A11, A29; :: thesis:

end;

hence A c= B1 by A3, A29, Th29; :: thesis:

end;

suppose for i being Element of Seg d holds
( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) ; :: thesis:

hence A c= B1 by A3, A4, A11, Th31; :: thesis:

end;

hence B1 in star A by A1; :: thesis:
A c= B2

proof

per cases by A23;

suppose A30: ( l2 . i0 < r2 . i0 & ( for i being Element of Seg d st i <> i0 holds
( l2 . i = l . i & r2 . i = r . i ) ) ) ; :: thesis:

A31: now

let i be Element of Seg d; :: thesis:
( i = i0 or ( i <> i0 & l2 . i = l . i & r2 . i = r . i ) ) by A30;
hence l2 . i <= r2 . i by A3, A30; :: thesis:

end;

now

let i be Element of Seg d; :: thesis:
( i = i0 or ( i <> i0 & l2 . i = l . i & r2 . i = r . i ) ) by A30;
hence ( l2 . i <= l . i & l . i <= r . i & r . i <= r2 . i ) by A3, A23, A31; :: thesis:

end;

hence A c= B2 by A3, A31, Th29; :: thesis:

end;

suppose for i being Element of Seg d holds
( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) ; :: thesis:

hence A c= B2 by A3, A4, A23, Th31; :: thesis:

end;

hence B2 in star A by A1; :: thesis:
A32: l1 <> l2 by A11, A23;
( for i being Element of Seg d holds l1 . i <= r1 . i or for i being Element of Seg d holds r1 . i < l1 . i ) by A14;
hence B1 <> B2 by A32, Th32; :: thesis:
let B be set ; :: thesis:
assume A33: B in star A ; :: thesis:
then reconsider B = B as Cell of d,G by A1;
consider l', r' being Element of REAL d such that
A34: ( B = cell l',r' & ( for i being Element of Seg d holds [(l' . i),(r' . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l' . i < r' . i or for i being Element of Seg d holds r' . i < l' . i ) ) by Th40;
A35: ( [(l' . i0),(r' . i0)] is Gap of G . i0 & [(l1 . i0),(l . i0)] is Gap of G . i0 & [(l . i0),(r2 . i0)] is Gap of G . i0 ) by A11, A23, A34;
A36: A c= B by A33, Th51;

per cases by A34;

suppose A37: for i being Element of Seg d holds l' . i < r' . i ; :: thesis:

A38: now

let i be Element of Seg d; :: thesis:
assume A39: i <> i0 ; :: thesis:
l' . i < r' . i by A37;
then ( ( l . i = l' . i & r . i = r' . i ) or ( l . i = l' . i & r . i = l' . i ) or ( l . i = r' . i & r . i = r' . i ) ) by A2, A3, A34, A36, Th46;
hence ( l' . i = l . i & r' . i = r . i ) by A3, A39; :: thesis:

end;

thus ( B = B1 or B = B2 ) :: thesis:

proof

A40: l' . i0 < r' . i0 by A37;

per cases by A2, A3, A34, A36, A40, Th46;

suppose A41: ( l . i0 = r' . i0 & r . i0 = r' . i0 ) ; :: thesis:

then A42: l' . i0 = l1 . i0 by A35, Th22;
reconsider l' = l', r' = r', l1 = l1, r1 = r1 as Function of (Seg d),REAL by Def4;

now

let i be Element of Seg d; :: thesis:
A43: l1 . i0 < l . i0 by A37, A41, A42;
then ( i = i0 or ( i <> i0 & l' . i = l . i & l1 . i = l . i ) ) by A11, A38;
hence l' . i = l1 . i by A35, A41, Th22; :: thesis:
( i = i0 or ( i <> i0 & r' . i = r . i & r1 . i = r . i ) ) by A11, A38, A43;
hence r' . i = r1 . i by A11, A41; :: thesis:

end;

then ( l' = l1 & r' = r1 ) by FUNCT_2:113;
hence ( B = B1 or B = B2 ) by A34; :: thesis:

end;

suppose A44: ( l . i0 = l' . i0 & r . i0 = l' . i0 ) ; :: thesis:

then A45: r' . i0 = r2 . i0 by A35, Th21;
reconsider l' = l', r' = r', l2 = l2, r2 = r2 as Function of (Seg d),REAL by Def4;

now

let i be Element of Seg d; :: thesis:
A46: l . i0 < r2 . i0 by A37, A44, A45;
then ( i = i0 or ( i <> i0 & r' . i = r . i & r2 . i = r . i ) ) by A23, A38;
hence r' . i = r2 . i by A35, A44, Th21; :: thesis:
( i = i0 or ( i <> i0 & l' . i = l . i & l2 . i = l . i ) ) by A23, A38, A46;
hence l' . i = l2 . i by A23, A44; :: thesis:

end;

then ( l' = l2 & r' = r2 ) by FUNCT_2:113;
hence ( B = B1 or B = B2 ) by A34; :: thesis:

end;

suppose A47: for i being Element of Seg d holds r' . i < l' . i ; :: thesis:

consider i1 being Element of Seg d such that
A48: ( ( l . i1 = l' . i1 & r . i1 = l' . i1 ) or ( l . i1 = r' . i1 & r . i1 = r' . i1 ) ) by A2, A3, A34, A36, Th47;
A49: i0 = i1 by A3, A48;
thus ( B = B1 or B = B2 ) :: thesis:

proof

per cases by A48, A49;

suppose A50: ( l . i0 = r' . i0 & r . i0 = r' . i0 ) ; :: thesis:

then l' . i0 = l1 . i0 by A35, Th22;
then B1 = infinite-cell G by A11, A47, A50, Th49;
hence ( B = B1 or B = B2 ) by A34, A47, Th49; :: thesis:

end;

suppose A51: ( l . i0 = l' . i0 & r . i0 = l' . i0 ) ; :: thesis:

then r' . i0 = r2 . i0 by A35, Th21;
then B2 = infinite-cell G by A23, A47, A51, Th49;
hence ( B = B1 or B = B2 ) by A34, A47, Th49; :: thesis:

end;

hence card (star A) = 2 by Th6; :: thesis: