set P = { p where p is Point of [:I[01],I[01]:] : p `2 <= 1 - (2 * (p `1)) } ;
thus IAA 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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IAA or x in { p where p is Point of [:I[01],I[01]:] : p `2 <= 1 - (2 * (p `1)) } )
assume A1: x in IAA ; :: thesis: x in { p where p is Point of [:I[01],I[01]:] : p `2 <= 1 - (2 * (p `1)) }
then reconsider x9 = x as Point of [:I[01],I[01]:] ;
consider a, b being Point of I[01] such that
A2: x = [a,b] and
A3: b <= 1 - (2 * a) by A1, Def8;
( x9 `1 = a & x9 `2 = b ) by A2;
hence x in { p where p is Point of [:I[01],I[01]:] : p `2 <= 1 - (2 * (p `1)) } by A3; :: 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 )
assume x in { p where p is Point of [:I[01],I[01]:] : p `2 <= 1 - (2 * (p `1)) } ; :: thesis: x in IAA
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 x in [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then A6: x = [(x `1),(x `2)] by MCART_1:21;
( p `1 is Point of I[01] & p `2 is Point of I[01] ) by Th27;
hence x in IAA by A4, A5, A6, Def8; :: thesis: verum