set KK = { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) } ;
thus IAA /\ IBB c= { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) } :: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) } c= IAA /\ IBB

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in IAA /\ IBB or x in { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) } )
assume A1: x in IAA /\ IBB ; :: thesis: x in { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) }
then x in IAA by XBOOLE_0:def 4;
then consider p being Point of [:I[01] ,I[01] :] such that
A2: x = p and
A3: p `2 <= 1 - (2 * (p `1 )) by Th61;
x in IBB by A1, XBOOLE_0:def 4;
then ex q being Point of [:I[01] ,I[01] :] st
( x = q & q `2 >= 1 - (2 * (q `1 )) & q `2 >= (2 * (q `1 )) - 1 ) by Th62;
then p `2 = 1 - (2 * (p `1 )) by A2, A3, XXREAL_0:1;
hence x in { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) } by A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) } or x in IAA /\ IBB )
assume x in { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) } ; :: thesis: x in IAA /\ IBB
then consider p being Point of [:I[01] ,I[01] :] such that
A4: p = x and
A5: p `2 = 1 - (2 * (p `1 )) ;
x in the carrier of [:I[01] ,I[01] :] by A4;
then A6: x in [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
then A7: ( x = [(p `1 ),(p `2 )] & p `1 in the carrier of I[01] ) by A4, MCART_1:10, MCART_1:23;
A8: p `2 in the carrier of I[01] by A4, A6, MCART_1:10;
then A9: x in IAA by A5, A7, Def10;
1 - (2 * (p `1 )) >= 0 by A5, A8, BORSUK_1:86;
then 0 + (2 * (p `1 )) <= 1 by XREAL_1:21;
then (2 * (p `1 )) / 2 <= 1 / 2 by XREAL_1:74;
then ( (2 * (p `1 )) - 1 <= 0 & 0 <= 1 - (2 * (p `1 )) ) by XREAL_1:219, XREAL_1:220;
then x in IBB by A5, A7, A8, Def11;
hence x in IAA /\ IBB by A9, XBOOLE_0:def 4; :: thesis: verum