let d be non zero Element of NAT ; :: thesis: for G being Grating of d
for B being Cell of (0 + 1),G holds card (del {B}) = 2
A1: ( 0 <= d & 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 & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) by Th44;
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, Th36;
then reconsider A1 = cell l,l, A2 = cell r,r as Cell of 0 ,G by Th39;
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 ) ) )
A3: ( A1 = {l} & A2 = {r} ) by Th28;
( l in B & r in B ) by A2, Th27;
then ( {l} c= B & {r} c= B ) by ZFMISC_1:37;
hence ( A1 in del {B} & A2 in del {B} ) by A1, A3, Th54; :: thesis: ( A1 <> A2 & ( for A being set holds
( not A in del {B} or A = A1 or A = A2 ) ) )
thus A1 <> A2 by A2, A3, ZFMISC_1:6; :: 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 A4: A in del {B} ; :: thesis: ( A = A1 or A = A2 )
then reconsider A = A as Cell of 0 ,G ;
A5: A c= B by A1, A4, Th54;
consider x being Element of REAL d such that
A6: ( A = cell x,x & ( for i being Element of Seg d holds x . i in G . i ) ) by Th38;
A7: x in A by A6, Th27;

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

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

A9: now

let i be Element of Seg d; :: thesis: l . i <= r . i
( i = i0 or i <> i0 ) ;
hence l . i <= r . i by A2, A8; :: thesis: verum

end;

x . i0 in G . i0 by A6;
then A10: ( l . i0 <= x . i0 & x . i0 <= r . i0 & ( not l . i0 < x . i0 or not x . i0 < r . i0 ) ) by A2, A5, A7, A9, Th17, Th25;

A11: now

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 ( l . i = r . i & l . i <= x . i & x . i <= r . i ) by A2, A5, A7, A9, Th25;
hence ( x . i = l . i & x . i = r . i ) by 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 A10, XXREAL_0:1;

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

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

now

let i be Element of Seg d; :: thesis: x . i = l . i
( i = i0 or i <> i0 ) ;
hence x . i = l . i by A11, A12; :: thesis: verum

end;

then x = l by FUNCT_2:113;
hence ( A = A1 or A = A2 ) by A6; :: thesis: verum

end;

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

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

now

let i be Element of Seg d; :: thesis: x . i = r . i
( i = i0 or i <> i0 ) ;
hence x . i = r . i by A11, A13; :: thesis: verum

end;

then x = r by FUNCT_2:113;
hence ( A = A1 or A = A2 ) by A6; :: thesis: verum

end;

end;

end;

end;

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

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

proof

let i be Element of Seg d; :: thesis: i = i0
( 1 <= i & i <= d & 1 <= i0 & i0 <= d ) by FINSEQ_1:3;
then ( i = 1 & i0 = 1 ) by A14, XXREAL_0:1;
hence i = i0 ; :: thesis: verum

end;

consider i1 being Element of Seg d such that
A16: ( r . i1 < l . i1 & ( x . i1 <= r . i1 or l . i1 <= x . i1 ) ) by A2, A5, A7, A14, Th26;
A17: i1 = i0 by A15;
x . i0 in G . i0 by A6;
then A18: ( not x . i0 < r . i0 & not l . i0 < x . i0 ) by A2, A14, Th17;
thus ( A = A1 or A = A2 ) :: thesis: verum

proof

per cases ( x . i0 = r . i0 or x . i0 = l . i0 ) by A16, A17, A18, XXREAL_0:1;

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

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

now

let i be Element of Seg d; :: thesis: x . i = r . i
i = i0 by A15;
hence x . i = r . i by A19; :: thesis: verum

end;

then x = r by FUNCT_2:113;
hence ( A = A1 or A = A2 ) by A6; :: thesis: verum

end;

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

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

now

let i be Element of Seg d; :: thesis: x . i = l . i
i = i0 by A15;
hence x . i = l . i by A20; :: thesis: verum

end;

then x = l by FUNCT_2:113;
hence ( A = A1 or A = A2 ) by A6; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence card (del {B}) = 2 by Th6; :: thesis: verum