set GG = [:I[01] ,I[01] :];
set SS = [:R^1 ,R^1 :];
( 0 in the carrier of I[01] & 1 in the carrier of I[01] ) by BORSUK_1:86;
then [1,0 ] in [:the carrier of I[01] ,the carrier of I[01] :] by ZFMISC_1:106;
then reconsider x = [1,0 ] as Point of [:I[01] ,I[01] :] by BORSUK_1:def 5;
reconsider PA = { p where p is Point of [:R^1 ,R^1 :] : p `2 <= (2 * (p `1 )) - 1 } as closed Subset of [:R^1 ,R^1 :] by Th26;
set P0 = { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } ;
A1: [:I[01] ,I[01] :] is SubSpace of [:R^1 ,R^1 :] by BORSUK_3:25;
A2: { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } = PA /\ ([#] [:I[01] ,I[01] :])

proof

thus { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } c= PA /\ ([#] [:I[01] ,I[01] :]) :: according to XBOOLE_0:def 10 :: thesis: PA /\ ([#] [:I[01] ,I[01] :]) c= { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 }

proof

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 <= (2 * (p `1 )) - 1 } or x in PA /\ ([#] [:I[01] ,I[01] :]) )
A3: the carrier of [:I[01] ,I[01] :] c= the carrier of [:R^1 ,R^1 :] by A1, BORSUK_1:35;
assume x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } ; :: thesis: x in PA /\ ([#] [:I[01] ,I[01] :])
then A4: ex p being Point of [:I[01] ,I[01] :] st
( x = p & p `2 <= (2 * (p `1 )) - 1 ) ;
then x in the carrier of [:I[01] ,I[01] :] ;
then reconsider a = x as Point of [:R^1 ,R^1 :] by A3;
a `2 <= (2 * (a `1 )) - 1 by A4;
then x in PA ;
hence x in PA /\ ([#] [:I[01] ,I[01] :]) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PA /\ ([#] [:I[01] ,I[01] :]) or x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } )
assume A5: x in PA /\ ([#] [:I[01] ,I[01] :]) ; :: thesis: x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 }
then x in PA by XBOOLE_0:def 4;
then ex p being Point of [:R^1 ,R^1 :] st
( x = p & p `2 <= (2 * (p `1 )) - 1 ) ;
hence x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } by A5; :: thesis: verum

end;

x `1 = 1 by MCART_1:7;
then x `2 <= (2 * (x `1 )) - 1 by MCART_1:7;
then x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } ;
hence { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } is non empty closed Subset of [:I[01] ,I[01] :] by A1, A2, PRE_TOPC:43; :: thesis: verum