let d9 be Nat; :: thesis:
let d be non zero 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, Th38;

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 Element of REAL such that
A8: [l1i0,(l . i0)] is Gap of G . i0 by A5, Th16;

per cases by A8, Th13;

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

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

proof

let i be Element of Seg d; :: thesis:
A11: l . i in REAL by XREAL_0:def 1;
( i = i0 or i <> i0 ) ;
hence ex li being Element of REAL st S₁[i,li] by A11; :: thesis:

end;

consider l1 being Function of (Seg d),REAL such that
A12: 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 Def3;
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, A12; :: thesis:

end;

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

consider l1, r1 being Element of REAL d such that
cell (l1,r1) = infinite-cell G and
A14: for i being Element of Seg d holds
( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) by Def10;
take l1 ; :: thesis:
take r1 ; :: thesis:
A15: r1 . i0 < l1 . i0 by A14;
[(l1 . i0),(r1 . i0)] is Gap of G . i0 by A14;
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, A13, A14, A15, Th19; :: thesis:

end;

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

A19: now :: thesis:

let i be Element of Seg d; :: thesis:
A20: ( 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 A16, A18, A20; :: thesis:

end;

A21: ( 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 A18;

suppose A22: ( 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 :: thesis:

let i be Element of Seg d; :: thesis:
A23: ( 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 A22, A23; :: 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 A19, Th37;
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 Element of REAL such that
A24: [(l . i0),r2i0] is Gap of G . i0 by A5, Th15;

per cases by A24, Th13;

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

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

proof

let i be Element of Seg d; :: thesis:
A27: r . i in REAL by XREAL_0:def 1;
( i = i0 or i <> i0 ) ;
hence ex ri being Element of REAL st S₁[i,ri] by A27; :: thesis:

end;

consider r2 being Function of (Seg d),REAL such that
A28: for i being Element of Seg d holds S₁[i,r2 . i] from FUNCT_2:sch 3(A26);
reconsider r2 = r2 as Element of REAL d by Def3;
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 A24, A25, A28; :: thesis:

end;

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

consider l2, r2 being Element of REAL d such that
cell (l2,r2) = infinite-cell G and
A30: for i being Element of Seg d holds
( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) by Def10;
take l2 ; :: thesis:
take r2 ; :: thesis:
A31: r2 . i0 < l2 . i0 by A30;
[(l2 . i0),(r2 . i0)] is Gap of G . i0 by A30;
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 A24, A29, A30, A31, Th19; :: thesis:

end;

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

A35: now :: thesis:

let i be Element of Seg d; :: thesis:
A36: ( 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 A32, A34, A36; :: 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 A34;

suppose A37: ( 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 :: thesis:

let i be Element of Seg d; :: thesis:
A38: ( 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 A37, A38; :: 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 A35, Th37;
take B1 ; :: thesis:
take B2 ; :: thesis:
A c= B1

proof

per cases by A18;

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

A40: now :: thesis:

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

end;

now :: thesis:

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

end;

hence A c= B1 by A3, A40, Th25; :: 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, A17, Th27; :: thesis:

end;

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

proof

per cases by A34;

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

A42: now :: thesis:

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

end;

now :: thesis:

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

end;

hence A c= B2 by A3, A42, Th25; :: 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, A33, Th27; :: thesis:

end;

hence B2 in star A by A1; :: thesis:
A43: l1 <> l2 by A17, A18, A33;
( 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 A21;
hence B1 <> B2 by A43, Th28; :: thesis:
let B be set ; :: thesis:
assume A44: 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
A45: B = cell (l9,r9) and
A46: for i being Element of Seg d holds [(l9 . i),(r9 . i)] is Gap of G . i and
A47: ( 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 Th36;
A48: [(l9 . i0),(r9 . i0)] is Gap of G . i0 by A46;
A49: A c= B by A44, Th47;

per cases by A47;

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

A51: now :: thesis:

let i be Element of Seg d; :: thesis:
assume A52: i <> i0 ; :: thesis:
l9 . i < r9 . i by A50;
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, A45, A49, Th42;
hence ( l9 . i = l . i & r9 . i = r . i ) by A6, A52; :: thesis:

end;

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

proof

A53: l9 . i0 < r9 . i0 by A50;

per cases by A2, A3, A4, A45, A49, A53, Th42;

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

then A55: l9 . i0 = l1 . i0 by A16, A17, A48, Th18;
reconsider l9 = l9, r9 = r9, l1 = l1, r1 = r1 as Function of (Seg d),REAL by Def3;

A56: now :: thesis:

let i be Element of Seg d; :: thesis:
A57: l1 . i0 < l . i0 by A50, A54, A55;
then ( i = i0 or ( i <> i0 & l9 . i = l . i & l1 . i = l . i ) ) by A17, A18, A51;
hence l9 . i = l1 . i by A16, A17, A48, A54, Th18; :: thesis:
( i = i0 or ( i <> i0 & r9 . i = r . i & r1 . i = r . i ) ) by A17, A18, A51, A57;
hence r9 . i = r1 . i by A17, A54; :: thesis:

end;

then l9 = l1 by FUNCT_2:63;
hence ( B = B1 or B = B2 ) by A45, A56, FUNCT_2:63; :: thesis:

end;

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

then A59: r9 . i0 = r2 . i0 by A32, A33, A48, Th17;
reconsider l9 = l9, r9 = r9, l2 = l2, r2 = r2 as Function of (Seg d),REAL by Def3;

A60: now :: thesis:

let i be Element of Seg d; :: thesis:
A61: l . i0 < r2 . i0 by A50, A58, A59;
then ( i = i0 or ( i <> i0 & r9 . i = r . i & r2 . i = r . i ) ) by A33, A34, A51;
hence r9 . i = r2 . i by A32, A33, A48, A58, Th17; :: thesis:
( i = i0 or ( i <> i0 & l9 . i = l . i & l2 . i = l . i ) ) by A33, A34, A51, A61;
hence l9 . i = l2 . i by A33, A58; :: thesis:

end;

then l9 = l2 by FUNCT_2:63;
hence ( B = B1 or B = B2 ) by A45, A60, FUNCT_2:63; :: thesis:

end;

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

consider i1 being Element of Seg d such that
A63: ( ( l . i1 = l9 . i1 & r . i1 = l9 . i1 ) or ( l . i1 = r9 . i1 & r . i1 = r9 . i1 ) ) by A2, A3, A45, A49, Th43;
A64: i0 = i1 by A6, A63;
thus ( B = B1 or B = B2 ) :: thesis:

proof

per cases by A63, A64;

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

then l9 . i0 = l1 . i0 by A16, A17, A48, Th18;
then B1 = infinite-cell G by A17, A18, A62, A65, Th45;
hence ( B = B1 or B = B2 ) by A45, A62, Th45; :: thesis:

end;

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

then r9 . i0 = r2 . i0 by A32, A33, A48, Th17;
then B2 = infinite-cell G by A33, A34, A62, A66, Th45;
hence ( B = B1 or B = B2 ) by A45, A62, Th45; :: thesis:

end;

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