let d9 be Element of NAT ; :: thesis:
let d be non zero Element of NAT ; :: thesis:
let G be Grating of d; :: thesis:
assume A1: d = d9 + 1 ; :: thesis:
then A2: d9 < d by NAT_1:13;
let A be Cell of d9,G; :: thesis:
consider l, r being Element of REAL d, i0 being Element of Seg d such that
A3: A = cell l,r and
A4: l . i0 = r . i0 and
A5: l . i0 in G . i0 and
A6: 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;

A7: now

let i be Element of Seg d; :: thesis:
( i = i0 or i <> i0 ) ;
hence l . i <= r . i by A4, A6; :: 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
A8: [l1i0,(l . i0)] is Gap of G . i0 by A5, Th20;

per cases by A8, Th17;

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

defpred S₁[ Element of Seg d, Real] means ( ( $1 = i0 implies $2 = l1i0 ) & ( $1 <> i0 implies $2 = l . $1 ) );
A10: 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
A11: for i being Element of Seg d holds S₁[i,l1 . i] from FUNCT_2:sch 3(A10);
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 A4, A8, A9, A11; :: thesis:

end;

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

consider l1, r1 being Element of REAL d such that
cell l1,r1 = infinite-cell G and
A13: 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:
A14: r1 . i0 < l1 . i0 by A13;
[(l1 . i0),(r1 . i0)] is Gap of G . i0 by A13;
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 A8, A12, A13, A14, Th23; :: thesis:

end;

then consider l1, r1 being Element of REAL d such that
A15: [(l1 . i0),(r1 . i0)] is Gap of G . i0 and
A16: r1 . i0 = l . i0 and
A17: ( ( 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 ) ) ;

A18: now

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

end;

A20: ( 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 A17;

suppose A21: ( 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:
A22: ( i <> i0 & l1 . i = l . i & r1 . i = r . i implies l1 . i < r1 . i ) by A6;
( i = i0 or i <> i0 ) ;
hence l1 . i < r1 . i by A21, A22; :: 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 A18, 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
A23: [(l . i0),r2i0] is Gap of G . i0 by A5, Th19;

per cases by A23, Th17;

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

defpred S₁[ Element of Seg d, Real] means ( ( $1 = i0 implies $2 = r2i0 ) & ( $1 <> i0 implies $2 = r . $1 ) );
A25: 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
A26: for i being Element of Seg d holds S₁[i,r2 . i] from FUNCT_2:sch 3(A25);
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 A23, A24, A26; :: thesis:

end;

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

consider l2, r2 being Element of REAL d such that
cell l2,r2 = infinite-cell G and
A28: 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:
A29: r2 . i0 < l2 . i0 by A28;
[(l2 . i0),(r2 . i0)] is Gap of G . i0 by A28;
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 A23, A27, A28, A29, Th23; :: thesis:

end;

then consider l2, r2 being Element of REAL d such that
A30: [(l2 . i0),(r2 . i0)] is Gap of G . i0 and
A31: l2 . i0 = l . i0 and
A32: ( ( 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 ) ) ;

A33: now

let i be Element of Seg d; :: thesis:
A34: ( i <> i0 & l2 . i = l . i & r2 . i = r . i implies [(l2 . i),(r2 . i)] is Gap of G . i ) by A6;
( i = i0 or i <> i0 ) ;
hence [(l2 . i),(r2 . i)] is Gap of G . i by A30, A32, A34; :: 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 A32;

suppose A35: ( 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:
A36: ( i <> i0 & l2 . i = l . i & r2 . i = r . i implies l2 . i < r2 . i ) by A6;
( i = i0 or i <> i0 ) ;
hence l2 . i < r2 . i by A35, A36; :: 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 A33, Th41;
take B1 ; :: thesis:
take B2 ; :: thesis:
A c= B1

proof

per cases by A17;

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

A38: now

let i be Element of Seg d; :: thesis:
( i = i0 or ( i <> i0 & l1 . i = l . i & r1 . i = r . i ) ) by A37;
hence l1 . i <= r1 . i by A6, A37; :: 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 A37;
hence ( l1 . i <= l . i & l . i <= r . i & r . i <= r1 . i ) by A4, A16, A38; :: thesis:

end;

hence A c= B1 by A3, A38, 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, A7, A16, Th31; :: thesis:

end;

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

proof

per cases by A32;

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

A40: now

let i be Element of Seg d; :: thesis:
( i = i0 or ( i <> i0 & l2 . i = l . i & r2 . i = r . i ) ) by A39;
hence l2 . i <= r2 . i by A6, A39; :: 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 A39;
hence ( l2 . i <= l . i & l . i <= r . i & r . i <= r2 . i ) by A4, A31, A40; :: thesis:

end;

hence A c= B2 by A3, A40, 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, A7, A31, Th31; :: thesis:

end;

hence B2 in star A by A1; :: thesis:
A41: l1 <> l2 by A16, A17, A31;
( 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 A20;
hence B1 <> B2 by A41, Th32; :: thesis:
let B be set ; :: thesis:
assume A42: B in star A ; :: thesis:
then reconsider B = B as Cell of d,G by A1;
consider l9, r9 being Element of REAL d such that
A43: B = cell l9,r9 and
A44: for i being Element of Seg d holds [(l9 . i),(r9 . i)] is Gap of G . i and
A45: ( for i being Element of Seg d holds l9 . i < r9 . i or for i being Element of Seg d holds r9 . i < l9 . i ) by Th40;
A46: [(l9 . i0),(r9 . i0)] is Gap of G . i0 by A44;
A47: A c= B by A42, Th51;

per cases by A45;

suppose A48: for i being Element of Seg d holds l9 . i < r9 . i ; :: thesis:

A49: now

let i be Element of Seg d; :: thesis:
assume A50: i <> i0 ; :: thesis:
l9 . i < r9 . i by A48;
then ( ( l . i = l9 . i & r . i = r9 . i ) or ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) by A2, A3, A43, A47, Th46;
hence ( l9 . i = l . i & r9 . i = r . i ) by A6, A50; :: thesis:

end;

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

proof

A51: l9 . i0 < r9 . i0 by A48;

per cases by A2, A3, A4, A43, A47, A51, Th46;

suppose A52: ( l . i0 = r9 . i0 & r . i0 = r9 . i0 ) ; :: thesis:

then A53: l9 . i0 = l1 . i0 by A15, A16, A46, Th22;
reconsider l9 = l9, r9 = r9, l1 = l1, r1 = r1 as Function of (Seg d),REAL by Def4;

A54: now

let i be Element of Seg d; :: thesis:
A55: l1 . i0 < l . i0 by A48, A52, A53;
then ( i = i0 or ( i <> i0 & l9 . i = l . i & l1 . i = l . i ) ) by A16, A17, A49;
hence l9 . i = l1 . i by A15, A16, A46, A52, Th22; :: thesis:
( i = i0 or ( i <> i0 & r9 . i = r . i & r1 . i = r . i ) ) by A16, A17, A49, A55;
hence r9 . i = r1 . i by A16, A52; :: thesis:

end;

then l9 = l1 by FUNCT_2:113;
hence ( B = B1 or B = B2 ) by A43, A54, FUNCT_2:113; :: thesis:

end;

suppose A56: ( l . i0 = l9 . i0 & r . i0 = l9 . i0 ) ; :: thesis:

then A57: r9 . i0 = r2 . i0 by A30, A31, A46, Th21;
reconsider l9 = l9, r9 = r9, l2 = l2, r2 = r2 as Function of (Seg d),REAL by Def4;

A58: now

let i be Element of Seg d; :: thesis:
A59: l . i0 < r2 . i0 by A48, A56, A57;
then ( i = i0 or ( i <> i0 & r9 . i = r . i & r2 . i = r . i ) ) by A31, A32, A49;
hence r9 . i = r2 . i by A30, A31, A46, A56, Th21; :: thesis:
( i = i0 or ( i <> i0 & l9 . i = l . i & l2 . i = l . i ) ) by A31, A32, A49, A59;
hence l9 . i = l2 . i by A31, A56; :: thesis:

end;

then l9 = l2 by FUNCT_2:113;
hence ( B = B1 or B = B2 ) by A43, A58, FUNCT_2:113; :: thesis:

end;

suppose A60: for i being Element of Seg d holds r9 . i < l9 . i ; :: thesis:

consider i1 being Element of Seg d such that
A61: ( ( l . i1 = l9 . i1 & r . i1 = l9 . i1 ) or ( l . i1 = r9 . i1 & r . i1 = r9 . i1 ) ) by A2, A3, A43, A47, Th47;
A62: i0 = i1 by A6, A61;
thus ( B = B1 or B = B2 ) :: thesis:

proof

per cases by A61, A62;

suppose A63: ( l . i0 = r9 . i0 & r . i0 = r9 . i0 ) ; :: thesis:

then l9 . i0 = l1 . i0 by A15, A16, A46, Th22;
then B1 = infinite-cell G by A16, A17, A60, A63, Th49;
hence ( B = B1 or B = B2 ) by A43, A60, Th49; :: thesis:

end;

suppose A64: ( l . i0 = l9 . i0 & r . i0 = l9 . i0 ) ; :: thesis:

then r9 . i0 = r2 . i0 by A30, A31, A46, Th21;
then B2 = infinite-cell G by A31, A32, A60, A64, Th49;
hence ( B = B1 or B = B2 ) by A43, A60, Th49; :: thesis:

end;

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