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 object ; :: 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 Th53;
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 Th54;
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 object ; :: 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 2;
then A7: ( x = [(p `1),(p `2)] & p `1 in the carrier of I[01] ) by A4, MCART_1:10, MCART_1:21;
A8: p `2 in the carrier of I[01] by A4, A6, MCART_1:10;
then A9: x in IAA by A5, A7, Def8;
1 - (2 * (p `1)) >= 0 by A5, A8, BORSUK_1:43;
then 0 + (2 * (p `1)) <= 1 by XREAL_1:19;
then (2 * (p `1)) / 2 <= 1 / 2 by XREAL_1:72;
then ( (2 * (p `1)) - 1 <= 0 & 0 <= 1 - (2 * (p `1)) ) by XREAL_1:217, XREAL_1:218;
then x in IBB by A5, A7, A8, Def9;
hence x in IAA /\ IBB by A9, XBOOLE_0:def 4; :: thesis: verum