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 ) ) )
proof
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;
per cases ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) by A3;
suppose A16: l . i0 < r . i0 ; :: thesis: ( A = A1 or A = A2 )
A17: now :: thesis: for i being Element of Seg d holds l . i <= r . i
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;
A18: x . i0 in G . i0 by A14;
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 )
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;
thus ( A = A1 or A = A2 ) :: thesis: verum
proof
per cases ( x . i0 = l . i0 or x . i0 = r . i0 ) by A19, A20, A21, XXREAL_0:1;
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;
now :: thesis: for i being Element of Seg d holds x . i = l . i
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;
then x = l by FUNCT_2:63;
hence ( A = A1 or A = A2 ) by A13; :: thesis: verum
end;
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;
now :: thesis: for i being Element of Seg d holds x . i = r . i
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;
then x = r by FUNCT_2:63;
hence ( A = A1 or A = A2 ) by A13; :: thesis: verum
end;
end;
end;
end;
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 consider i1 being Element of Seg d such that
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
per cases ( x . i0 = r . i0 or x . i0 = l . i0 ) by A33, A34, A36, A37, XXREAL_0:1;
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;
now :: thesis: for i being Element of Seg d holds x . i = r . i
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;
then x = r by FUNCT_2:63;
hence ( A = A1 or A = A2 ) by A13; :: thesis: verum
end;
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;
now :: thesis: for i being Element of Seg d holds x . i = l . i
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;
then x = l by FUNCT_2:63;
hence ( A = A1 or A = A2 ) by A13; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence card (del {B}) = 2 by Th5; :: thesis: verum