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 object ; :: 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:40, MCART_1:10;
A2: x = [q,p] by A1, MCART_1:21;
( 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 :: thesis: ( x in IAA or x in IBB or x in ICC )

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, Def9; :: 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, Def10; :: 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, Def8; :: 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