set GG = [:I[01],I[01]:];
set SS = [:R^1,R^1:];
1 in the carrier of I[01] by BORSUK_1:43;
then [1,1] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then reconsider x = [1,1] as Point of [:I[01],I[01]:] by BORSUK_1:def 2;
reconsider PA = { p where p is Point of [:R^1,R^1:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } as closed Subset of [:R^1,R^1:] by Th23;
set P0 = { p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } ;
A1: x `2 >= (2 * (x `1)) - 1 ;
A2: [:I[01],I[01]:] is SubSpace of [:R^1,R^1:] by BORSUK_3:21;
A3: { p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & 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 >= 1 - (2 * (p `1)) & 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 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) }

proof

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

end;

let x be object ; :: 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 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } )
assume A6: x in PA /\ ([#] [:I[01],I[01]:]) ; :: thesis: x in { p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & 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 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) ;
hence x in { p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } by A6; :: thesis: verum

end;

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