thus (IAA \/ IBB ) \/ ICC c= [:[.0 ,1.],[.0 ,1.]:] by Th1; :: according to XBOOLE_0:def 10 :: thesis: [:[.0 ,1.],[.0 ,1.]:] c= (IAA \/ IBB ) \/ ICC
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:[.0 ,1.],[.0 ,1.]:] or x in (IAA \/ IBB ) \/ ICC )
assume A1: x in [:[.0 ,1.],[.0 ,1.]:] ; :: thesis: x in (IAA \/ IBB ) \/ ICC
then reconsider q = x `1 , p = x `2 as Point of I[01] by BORSUK_1:83, MCART_1:10;
A2: x = [q,p] by A1, MCART_1:23;
( x in IAA or x in IBB or x in ICC )

proof

per cases ( p >= 1 - (2 * q) or p < 1 - (2 * q) ) ;

suppose A3: p >= 1 - (2 * q) ; :: thesis: ( x in IAA or x in IBB or x in ICC )

now

per cases ( p >= (2 * q) - 1 or p < (2 * q) - 1 ) ;

suppose p >= (2 * q) - 1 ; :: thesis: ( x in IAA or x in IBB or x in ICC )

hence ( x in IAA or x in IBB or x in ICC ) by A2, A3, Def11; :: thesis: verum

end;

suppose p < (2 * q) - 1 ; :: thesis: ( x in IAA or x in IBB or x in ICC )

hence ( x in IAA or x in IBB or x in ICC ) by A2, Def12; :: thesis: verum

end;

end;

end;

hence ( x in IAA or x in IBB or x in ICC ) ; :: thesis: verum

end;

suppose p < 1 - (2 * q) ; :: thesis: ( x in IAA or x in IBB or x in ICC )

hence ( x in IAA or x in IBB or x in ICC ) by A2, Def10; :: thesis: verum

end;

end;

end;

then ( x in IAA \/ IBB or x in ICC ) by XBOOLE_0:def 3;
hence x in (IAA \/ IBB ) \/ ICC by XBOOLE_0:def 3; :: thesis: verum