let x be Point of I[01]; :: thesis: ( x < 1 / 2 implies ( not [x,0] in IBB & not [x,0] in ICC ) )
assume A1: x < 1 / 2 ; :: thesis: ( not [x,0] in IBB & not [x,0] in ICC )
thus not [x,0] in IBB :: thesis: not [x,0] in ICC

proof

assume [x,0] in IBB ; :: thesis: contradiction
then consider a, b being Point of I[01] such that
A2: [x,0] = [a,b] and
A3: b >= 1 - (2 * a) and
b >= (2 * a) - 1 by Def9;
( x = a & b = 0 ) by A2, XTUPLE_0:1;
then 0 + (2 * x) >= 1 by A3, XREAL_1:20;
then (2 * x) / 2 >= 1 / 2 by XREAL_1:72;
hence contradiction by A1; :: thesis: verum

end;

not [x,0] in ICC

proof

assume [x,0] in ICC ; :: thesis: contradiction
then consider a, b being Point of I[01] such that
A4: [x,0] = [a,b] and
A5: b <= (2 * a) - 1 by Def10;
( x = a & b = 0 ) by A4, XTUPLE_0:1;
then 0 + 1 <= 2 * x by A5, XREAL_1:19;
then 1 / 2 <= (2 * x) / 2 by XREAL_1:72;
hence contradiction by A1; :: thesis: verum

end;

hence not [x,0] in ICC ; :: thesis: verum