let d be non zero Nat; :: thesis: for G being Grating of d

for B being Cell of (0 + 1),G holds card (del {B}) = 2

A1: 0 + 1 <= d by Def2;

let G be Grating of d; :: thesis: for B being Cell of (0 + 1),G holds card (del {B}) = 2

let B be Cell of (0 + 1),G; :: thesis: card (del {B}) = 2

consider l, r being Element of REAL d, i0 being Element of Seg d such that

A2: B = cell (l,r) and

A3: ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) and

A4: [(l . i0),(r . i0)] is Gap of G . i0 and

A5: for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) by Th40;

ex A1, A2 being set st

( A1 in del {B} & A2 in del {B} & A1 <> A2 & ( for A being set holds

( not A in del {B} or A = A1 or A = A2 ) ) )

for B being Cell of (0 + 1),G holds card (del {B}) = 2

A1: 0 + 1 <= d by Def2;

let G be Grating of d; :: thesis: for B being Cell of (0 + 1),G holds card (del {B}) = 2

let B be Cell of (0 + 1),G; :: thesis: card (del {B}) = 2

consider l, r being Element of REAL d, i0 being Element of Seg d such that

A2: B = cell (l,r) and

A3: ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) and

A4: [(l . i0),(r . i0)] is Gap of G . i0 and

A5: for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) by Th40;

ex A1, A2 being set st

( A1 in del {B} & A2 in del {B} & A1 <> A2 & ( for A being set holds

( not A in del {B} or A = A1 or A = A2 ) ) )

proof

hence
card (del {B}) = 2
by Th5; :: thesis: verum
for i being Element of Seg d holds

( l . i in G . i & r . i in G . i ) by A1, A2, Th32;

then reconsider A1 = cell (l,l), A2 = cell (r,r) as Cell of 0,G by Th35;

take A1 ; :: thesis: ex A2 being set st

( A1 in del {B} & A2 in del {B} & A1 <> A2 & ( for A being set holds

( not A in del {B} or A = A1 or A = A2 ) ) )

take A2 ; :: thesis: ( A1 in del {B} & A2 in del {B} & A1 <> A2 & ( for A being set holds

( not A in del {B} or A = A1 or A = A2 ) ) )

A6: A1 = {l} by Th24;

A7: A2 = {r} by Th24;

A8: l in B by A2, Th23;

A9: r in B by A2, Th23;

A10: {l} c= B by A8, ZFMISC_1:31;

{r} c= B by A9, ZFMISC_1:31;

hence ( A1 in del {B} & A2 in del {B} ) by A1, A6, A7, A10, Th50; :: thesis: ( A1 <> A2 & ( for A being set holds

( not A in del {B} or A = A1 or A = A2 ) ) )

thus A1 <> A2 by A3, A6, A7, ZFMISC_1:3; :: thesis: for A being set holds

( not A in del {B} or A = A1 or A = A2 )

let A be set ; :: thesis: ( not A in del {B} or A = A1 or A = A2 )

assume A11: A in del {B} ; :: thesis: ( A = A1 or A = A2 )

then reconsider A = A as Cell of 0,G ;

A12: A c= B by A1, A11, Th50;

consider x being Element of REAL d such that

A13: A = cell (x,x) and

A14: for i being Element of Seg d holds x . i in G . i by Th34;

A15: x in A by A13, Th23;

end;( l . i in G . i & r . i in G . i ) by A1, A2, Th32;

then reconsider A1 = cell (l,l), A2 = cell (r,r) as Cell of 0,G by Th35;

take A1 ; :: thesis: ex A2 being set st

( A1 in del {B} & A2 in del {B} & A1 <> A2 & ( for A being set holds

( not A in del {B} or A = A1 or A = A2 ) ) )

take A2 ; :: thesis: ( A1 in del {B} & A2 in del {B} & A1 <> A2 & ( for A being set holds

( not A in del {B} or A = A1 or A = A2 ) ) )

A6: A1 = {l} by Th24;

A7: A2 = {r} by Th24;

A8: l in B by A2, Th23;

A9: r in B by A2, Th23;

A10: {l} c= B by A8, ZFMISC_1:31;

{r} c= B by A9, ZFMISC_1:31;

hence ( A1 in del {B} & A2 in del {B} ) by A1, A6, A7, A10, Th50; :: thesis: ( A1 <> A2 & ( for A being set holds

( not A in del {B} or A = A1 or A = A2 ) ) )

thus A1 <> A2 by A3, A6, A7, ZFMISC_1:3; :: thesis: for A being set holds

( not A in del {B} or A = A1 or A = A2 )

let A be set ; :: thesis: ( not A in del {B} or A = A1 or A = A2 )

assume A11: A in del {B} ; :: thesis: ( A = A1 or A = A2 )

then reconsider A = A as Cell of 0,G ;

A12: A c= B by A1, A11, Th50;

consider x being Element of REAL d such that

A13: A = cell (x,x) and

A14: for i being Element of Seg d holds x . i in G . i by Th34;

A15: x in A by A13, Th23;

per cases
( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) )
by A3;

end;

suppose A16:
l . i0 < r . i0
; :: thesis: ( A = A1 or A = A2 )

A19: l . i0 <= x . i0 by A2, A12, A15, A17, Th21;

A20: x . i0 <= r . i0 by A2, A12, A15, A17, Th21;

A21: ( not l . i0 < x . i0 or not x . i0 < r . i0 ) by A4, A18, Th13;

end;

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

A18:
x . i0 in G . i0
by A14;let i be Element of Seg d; :: thesis: l . i <= r . i

( i = i0 or i <> i0 ) ;

hence l . i <= r . i by A5, A16; :: thesis: verum

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

hence l . i <= r . i by A5, A16; :: thesis: verum

A19: l . i0 <= x . i0 by A2, A12, A15, A17, Th21;

A20: x . i0 <= r . i0 by A2, A12, A15, A17, Th21;

A21: ( not l . i0 < x . i0 or not x . i0 < r . i0 ) by A4, A18, Th13;

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

( x . i = l . i & x . i = r . i )

thus
( A = A1 or A = A2 )
:: thesis: verum( x . i = l . i & x . i = r . i )

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

assume i <> i0 ; :: thesis: ( x . i = l . i & x . i = r . i )

then A23: l . i = r . i by A5;

A24: l . i <= x . i by A2, A12, A15, A17, Th21;

x . i <= r . i by A2, A12, A15, A17, Th21;

hence ( x . i = l . i & x . i = r . i ) by A23, A24, XXREAL_0:1; :: thesis: verum

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

then A23: l . i = r . i by A5;

A24: l . i <= x . i by A2, A12, A15, A17, Th21;

x . i <= r . i by A2, A12, A15, A17, Th21;

hence ( x . i = l . i & x . i = r . i ) by A23, A24, XXREAL_0:1; :: thesis: verum

proof
end;

per cases
( x . i0 = l . i0 or x . i0 = r . i0 )
by A19, A20, A21, XXREAL_0:1;

end;

suppose A25:
x . i0 = l . i0
; :: thesis: ( A = A1 or A = A2 )

reconsider x = x, l = l as Function of (Seg d),REAL by Def3;

hence ( A = A1 or A = A2 ) by A13; :: thesis: verum

end;now :: thesis: for i being Element of Seg d holds x . i = l . i

then
x = l
by FUNCT_2:63;let i be Element of Seg d; :: thesis: x . i = l . i

( i = i0 or i <> i0 ) ;

hence x . i = l . i by A22, A25; :: thesis: verum

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

hence x . i = l . i by A22, A25; :: thesis: verum

hence ( A = A1 or A = A2 ) by A13; :: thesis: verum

suppose A26:
x . i0 = r . i0
; :: thesis: ( A = A1 or A = A2 )

reconsider x = x, r = r as Function of (Seg d),REAL by Def3;

hence ( A = A1 or A = A2 ) by A13; :: thesis: verum

end;now :: thesis: for i being Element of Seg d holds x . i = r . i

then
x = r
by FUNCT_2:63;let i be Element of Seg d; :: thesis: x . i = r . i

( i = i0 or i <> i0 ) ;

hence x . i = r . i by A22, A26; :: thesis: verum

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

hence x . i = r . i by A22, A26; :: thesis: verum

hence ( A = A1 or A = A2 ) by A13; :: thesis: verum

suppose A27:
( d = 1 & r . i0 < l . i0 )
; :: thesis: ( A = A1 or A = A2 )

A28:
for i being Element of Seg d holds i = i0

r . i1 < l . i1 and

A33: ( x . i1 <= r . i1 or l . i1 <= x . i1 ) by A2, A12, A15, A27, Th22;

A34: i1 = i0 by A28;

A35: x . i0 in G . i0 by A14;

then A36: not x . i0 < r . i0 by A4, A27, Th13;

A37: not l . i0 < x . i0 by A4, A27, A35, Th13;

thus ( A = A1 or A = A2 ) :: thesis: verum

end;proof

consider i1 being Element of Seg d such that
let i be Element of Seg d; :: thesis: i = i0

A29: 1 <= i by FINSEQ_1:1;

A30: i <= d by FINSEQ_1:1;

A31: 1 <= i0 by FINSEQ_1:1;

A32: i0 <= d by FINSEQ_1:1;

i = 1 by A27, A29, A30, XXREAL_0:1;

hence i = i0 by A27, A31, A32, XXREAL_0:1; :: thesis: verum

end;A29: 1 <= i by FINSEQ_1:1;

A30: i <= d by FINSEQ_1:1;

A31: 1 <= i0 by FINSEQ_1:1;

A32: i0 <= d by FINSEQ_1:1;

i = 1 by A27, A29, A30, XXREAL_0:1;

hence i = i0 by A27, A31, A32, XXREAL_0:1; :: thesis: verum

r . i1 < l . i1 and

A33: ( x . i1 <= r . i1 or l . i1 <= x . i1 ) by A2, A12, A15, A27, Th22;

A34: i1 = i0 by A28;

A35: x . i0 in G . i0 by A14;

then A36: not x . i0 < r . i0 by A4, A27, Th13;

A37: not l . i0 < x . i0 by A4, A27, A35, Th13;

thus ( A = A1 or A = A2 ) :: thesis: verum

proof
end;

per cases
( x . i0 = r . i0 or x . i0 = l . i0 )
by A33, A34, A36, A37, XXREAL_0:1;

end;

suppose A38:
x . i0 = r . i0
; :: thesis: ( A = A1 or A = A2 )

reconsider x = x, r = r as Function of (Seg d),REAL by Def3;

hence ( A = A1 or A = A2 ) by A13; :: thesis: verum

end;now :: thesis: for i being Element of Seg d holds x . i = r . i

then
x = r
by FUNCT_2:63;let i be Element of Seg d; :: thesis: x . i = r . i

i = i0 by A28;

hence x . i = r . i by A38; :: thesis: verum

end;i = i0 by A28;

hence x . i = r . i by A38; :: thesis: verum

hence ( A = A1 or A = A2 ) by A13; :: thesis: verum

suppose A39:
x . i0 = l . i0
; :: thesis: ( A = A1 or A = A2 )

reconsider x = x, l = l as Function of (Seg d),REAL by Def3;

hence ( A = A1 or A = A2 ) by A13; :: thesis: verum

end;now :: thesis: for i being Element of Seg d holds x . i = l . i

then
x = l
by FUNCT_2:63;let i be Element of Seg d; :: thesis: x . i = l . i

i = i0 by A28;

hence x . i = l . i by A39; :: thesis: verum

end;i = i0 by A28;

hence x . i = l . i by A39; :: thesis: verum

hence ( A = A1 or A = A2 ) by A13; :: thesis: verum