let d9 be Nat; :: thesis: for d being non zero Nat

for G being Grating of d st d = d9 + 1 holds

for A being Cell of d9,G holds card (star A) = 2

let d be non zero Nat; :: thesis: for G being Grating of d st d = d9 + 1 holds

for A being Cell of d9,G holds card (star A) = 2

let G be Grating of d; :: thesis: ( d = d9 + 1 implies for A being Cell of d9,G holds card (star A) = 2 )

assume A1: d = d9 + 1 ; :: thesis: for A being Cell of d9,G holds card (star A) = 2

then A2: d9 < d by NAT_1:13;

let A be Cell of d9,G; :: thesis: card (star A) = 2

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;

( 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 ) ) )

for G being Grating of d st d = d9 + 1 holds

for A being Cell of d9,G holds card (star A) = 2

let d be non zero Nat; :: thesis: for G being Grating of d st d = d9 + 1 holds

for A being Cell of d9,G holds card (star A) = 2

let G be Grating of d; :: thesis: ( d = d9 + 1 implies for A being Cell of d9,G holds card (star A) = 2 )

assume A1: d = d9 + 1 ; :: thesis: for A being Cell of d9,G holds card (star A) = 2

then A2: d9 < d by NAT_1:13;

let A be Cell of d9,G; :: thesis: card (star A) = 2

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;

A7: now :: thesis: for i being Element of Seg d holds l . i <= r . i

ex B1, B2 being set st let i be Element of Seg d; :: thesis: l . i <= r . i

( i = i0 or i <> i0 ) ;

hence l . i <= r . i by A4, A6; :: thesis: verum

end;( i = i0 or i <> i0 ) ;

hence l . i <= r . i by A4, A6; :: thesis: verum

( 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

hence
card (star A) = 2
by Th5; :: thesis: verum
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 ) ) )

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 ) ) ;

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 ) ) )

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 ) ) ;

take B1 ; :: thesis: ex 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 ) ) )

take B2 ; :: thesis: ( 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 ) ) )

A c= B1

( not B in star A or B = B1 or B = B2 ) ) )

A c= B2

( not B in star A or B = B1 or B = B2 ) ) )

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: for B being set holds

( not B in star A or B = B1 or B = B2 )

let B be set ; :: thesis: ( not B in star A or B = B1 or B = B2 )

assume A44: B in star A ; :: thesis: ( B = B1 or B = B2 )

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;

end;( [(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

then consider l1, r1 being Element of REAL d such that
consider l1i0 being Element of REAL such that

A8: [l1i0,(l . i0)] is Gap of G . i0 by A5, Th16;

end;A8: [l1i0,(l . i0)] is Gap of G . i0 by A5, Th16;

per cases
( l1i0 < l . i0 or l . i0 < l1i0 )
by A8, Th13;

end;

suppose A9:
l1i0 < l . i0
; :: thesis: 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 ) ) )

( [(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 ) ) )

defpred S_{1}[ 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_{1}[i,li]

A12: for i being Element of Seg d holds S_{1}[i,l1 . i]
from FUNCT_2:sch 3(A10);

reconsider l1 = l1 as Element of REAL d by Def3;

take l1 ; :: thesis: ex 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 ) ) )

take r ; :: thesis: ( [(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 ) ) )

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: verum

end;A10: for i being Element of Seg d ex li being Element of REAL st S

proof

consider l1 being Function of (Seg d),REAL such that
let i be Element of Seg d; :: thesis: ex li being Element of REAL st S_{1}[i,li]

A11: l . i in REAL by XREAL_0:def 1;

( i = i0 or i <> i0 ) ;

hence ex li being Element of REAL st S_{1}[i,li]
by A11; :: thesis: verum

end;A11: l . i in REAL by XREAL_0:def 1;

( i = i0 or i <> i0 ) ;

hence ex li being Element of REAL st S

A12: for i being Element of Seg d holds S

reconsider l1 = l1 as Element of REAL d by Def3;

take l1 ; :: thesis: ex 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 ) ) )

take r ; :: thesis: ( [(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 ) ) )

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: verum

suppose A13:
l . i0 < l1i0
; :: thesis: 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 ) ) )

( [(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 ) ) )

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: ex 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 ) ) )

take r1 ; :: thesis: ( [(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 ) ) )

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: verum

end;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: ex 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 ) ) )

take r1 ; :: thesis: ( [(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 ) ) )

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: verum

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: for i being Element of Seg d holds [(l1 . i),(r1 . i)] is Gap of G . i

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 )
let i be Element of Seg d; :: thesis: [(l1 . i),(r1 . i)] is Gap of G . i

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: verum

end;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: verum

proof
end;

then reconsider B1 = cell (l1,r1) as Cell of d,G by A19, Th37;per cases
( ( 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 A18;

end;

( 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 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: ( 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 )

end;

( l1 . i = l . i & r1 . i = r . i ) ) ) ; :: thesis: ( 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 )

now :: thesis: for i being Element of Seg d holds l1 . i < r1 . i

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: verumlet i be Element of Seg d; :: thesis: l1 . i < r1 . i

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: verum

end;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: verum

suppose
for i being Element of Seg d holds

( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) ; :: thesis: ( 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 )

( r1 . i < l1 . i & [(l1 . i),(r1 . i)] is Gap of G . i ) ; :: thesis: ( 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 )

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: verum

end;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

then consider l2, r2 being Element of REAL d such that
consider r2i0 being Element of REAL such that

A24: [(l . i0),r2i0] is Gap of G . i0 by A5, Th15;

end;A24: [(l . i0),r2i0] is Gap of G . i0 by A5, Th15;

per cases
( l . i0 < r2i0 or r2i0 < l . i0 )
by A24, Th13;

end;

suppose A25:
l . i0 < r2i0
; :: thesis: 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 ) ) )

( [(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 ) ) )

defpred S_{1}[ 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_{1}[i,ri]

A28: for i being Element of Seg d holds S_{1}[i,r2 . i]
from FUNCT_2:sch 3(A26);

reconsider r2 = r2 as Element of REAL d by Def3;

take l ; :: thesis: ex r2 being Element of REAL d st

( [(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 ) ) )

take r2 ; :: thesis: ( [(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 ) ) )

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: verum

end;A26: for i being Element of Seg d ex ri being Element of REAL st S

proof

consider r2 being Function of (Seg d),REAL such that
let i be Element of Seg d; :: thesis: ex ri being Element of REAL st S_{1}[i,ri]

A27: r . i in REAL by XREAL_0:def 1;

( i = i0 or i <> i0 ) ;

hence ex ri being Element of REAL st S_{1}[i,ri]
by A27; :: thesis: verum

end;A27: r . i in REAL by XREAL_0:def 1;

( i = i0 or i <> i0 ) ;

hence ex ri being Element of REAL st S

A28: for i being Element of Seg d holds S

reconsider r2 = r2 as Element of REAL d by Def3;

take l ; :: thesis: ex r2 being Element of REAL d st

( [(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 ) ) )

take r2 ; :: thesis: ( [(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 ) ) )

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: verum

suppose A29:
r2i0 < l . i0
; :: thesis: 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 ) ) )

( [(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 ) ) )

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: ex 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 ) ) )

take r2 ; :: thesis: ( [(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 ) ) )

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: verum

end;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: ex 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 ) ) )

take r2 ; :: thesis: ( [(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 ) ) )

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: verum

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: for i being Element of Seg d holds [(l2 . i),(r2 . i)] is Gap of G . i

( 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 )
let i be Element of Seg d; :: thesis: [(l2 . i),(r2 . i)] is Gap of G . i

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: verum

end;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: verum

proof
end;

then reconsider B2 = cell (l2,r2) as Cell of d,G by A35, Th37;per cases
( ( 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 A34;

end;

( 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 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: ( 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 )

end;

( l2 . i = l . i & r2 . i = r . i ) ) ) ; :: thesis: ( 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 )

now :: thesis: for i being Element of Seg d holds l2 . i < r2 . i

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: verumlet i be Element of Seg d; :: thesis: l2 . i < r2 . i

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: verum

end;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: verum

suppose
for i being Element of Seg d holds

( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) ; :: thesis: ( 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 )

( r2 . i < l2 . i & [(l2 . i),(r2 . i)] is Gap of G . i ) ; :: thesis: ( 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 )

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: verum

end;take B1 ; :: thesis: ex 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 ) ) )

take B2 ; :: thesis: ( 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 ) ) )

A c= B1

proof
end;

hence
B1 in star A
by A1; :: thesis: ( B2 in star A & B1 <> B2 & ( for B being set holds per cases
( ( 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 A18;

end;

( 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 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: A c= B1

end;

( l1 . i = l . i & r1 . i = r . i ) ) ) ; :: thesis: A c= B1

A40: now :: thesis: for i being Element of Seg d holds l1 . i <= r1 . i

let i be Element of Seg d; :: thesis: l1 . i <= r1 . i

( i = i0 or ( i <> i0 & l1 . i = l . i & r1 . i = r . i ) ) by A39;

hence l1 . i <= r1 . i by A6, A39; :: thesis: verum

end;( i = i0 or ( i <> i0 & l1 . i = l . i & r1 . i = r . i ) ) by A39;

hence l1 . i <= r1 . i by A6, A39; :: thesis: verum

now :: thesis: for i being Element of Seg d holds

( l1 . i <= l . i & l . i <= r . i & r . i <= r1 . i )

hence
A c= B1
by A3, A40, Th25; :: thesis: verum( l1 . i <= l . i & l . i <= r . i & r . i <= r1 . i )

let i be Element of Seg d; :: thesis: ( l1 . i <= l . i & l . i <= r . i & r . i <= r1 . i )

( 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: verum

end;( 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: verum

( not B in star A or B = B1 or B = B2 ) ) )

A c= B2

proof
end;

hence
B2 in star A
by A1; :: thesis: ( B1 <> B2 & ( for B being set holds per cases
( ( 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 A34;

end;

( 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 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: A c= B2

end;

( l2 . i = l . i & r2 . i = r . i ) ) ) ; :: thesis: A c= B2

A42: now :: thesis: for i being Element of Seg d holds l2 . i <= r2 . i

let i be Element of Seg d; :: thesis: l2 . i <= r2 . i

( i = i0 or ( i <> i0 & l2 . i = l . i & r2 . i = r . i ) ) by A41;

hence l2 . i <= r2 . i by A6, A41; :: thesis: verum

end;( i = i0 or ( i <> i0 & l2 . i = l . i & r2 . i = r . i ) ) by A41;

hence l2 . i <= r2 . i by A6, A41; :: thesis: verum

now :: thesis: for i being Element of Seg d holds

( l2 . i <= l . i & l . i <= r . i & r . i <= r2 . i )

hence
A c= B2
by A3, A42, Th25; :: thesis: verum( l2 . i <= l . i & l . i <= r . i & r . i <= r2 . i )

let i be Element of Seg d; :: thesis: ( l2 . i <= l . i & l . i <= r . i & r . i <= r2 . i )

( 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: verum

end;( 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: verum

( not B in star A or B = B1 or B = B2 ) ) )

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: for B being set holds

( not B in star A or B = B1 or B = B2 )

let B be set ; :: thesis: ( not B in star A or B = B1 or B = B2 )

assume A44: B in star A ; :: thesis: ( B = B1 or B = B2 )

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
( 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 A47;

end;

suppose A50:
for i being Element of Seg d holds l9 . i < r9 . i
; :: thesis: ( B = B1 or B = B2 )

end;

A51: now :: thesis: for i being Element of Seg d st i <> i0 holds

( l9 . i = l . i & r9 . i = r . i )

thus
( B = B1 or B = B2 )
:: thesis: verum( l9 . i = l . i & r9 . i = r . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l9 . i = l . i & r9 . i = r . i ) )

assume A52: i <> i0 ; :: thesis: ( l9 . i = l . i & r9 . i = r . i )

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: verum

end;assume A52: i <> i0 ; :: thesis: ( l9 . i = l . i & r9 . i = r . i )

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: verum

proof

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

end;per cases
( ( l . i0 = r9 . i0 & r . i0 = r9 . i0 ) or ( l . i0 = l9 . i0 & r . i0 = l9 . i0 ) )
by A2, A3, A4, A45, A49, A53, Th42;

end;

suppose A54:
( l . i0 = r9 . i0 & r . i0 = r9 . i0 )
; :: thesis: ( B = B1 or B = B2 )

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;

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

end;reconsider l9 = l9, r9 = r9, l1 = l1, r1 = r1 as Function of (Seg d),REAL by Def3;

A56: now :: thesis: for i being Element of Seg d holds

( l9 . i = l1 . i & r9 . i = r1 . i )

then
l9 = l1
by FUNCT_2:63;( l9 . i = l1 . i & r9 . i = r1 . i )

let i be Element of Seg d; :: thesis: ( l9 . i = l1 . i & r9 . i = r1 . i )

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: r9 . i = r1 . i

( 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: verum

end;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: r9 . i = r1 . i

( 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: verum

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

suppose A58:
( l . i0 = l9 . i0 & r . i0 = l9 . i0 )
; :: thesis: ( B = B1 or B = B2 )

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;

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

end;reconsider l9 = l9, r9 = r9, l2 = l2, r2 = r2 as Function of (Seg d),REAL by Def3;

A60: now :: thesis: for i being Element of Seg d holds

( r9 . i = r2 . i & l9 . i = l2 . i )

then
l9 = l2
by FUNCT_2:63;( r9 . i = r2 . i & l9 . i = l2 . i )

let i be Element of Seg d; :: thesis: ( r9 . i = r2 . i & l9 . i = l2 . i )

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: l9 . i = l2 . i

( 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: verum

end;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: l9 . i = l2 . i

( 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: verum

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

suppose A62:
for i being Element of Seg d holds r9 . i < l9 . i
; :: thesis: ( B = B1 or B = B2 )

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: verum

end;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: verum

proof
end;

per cases
( ( l . i0 = r9 . i0 & r . i0 = r9 . i0 ) or ( l . i0 = l9 . i0 & r . i0 = l9 . i0 ) )
by A63, A64;

end;