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] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) by Def11;
( x = a & b = 0 ) by A2, ZFMISC_1:33;
then 0 + (2 * x) >= 1 by A2, XREAL_1:22;
then (2 * x) / 2 >= 1 / 2 by XREAL_1:74;
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
A3: ( [x,0 ] = [a,b] & b <= (2 * a) - 1 ) by Def12;
( x = a & b = 0 ) by A3, ZFMISC_1:33;
then 0 + 1 <= 2 * x by A3, XREAL_1:21;
then 1 / 2 <= (2 * x) / 2 by XREAL_1:74;
hence contradiction by A1; :: thesis: verum

end;

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