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:43;
then
[1,0] in [: the carrier of I[01], the carrier of I[01]:]
by ZFMISC_1:87;
then reconsider x = [1,0] 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 <= (2 * (p `1)) - 1 } as closed Subset of [:R^1,R^1:] by Th22;
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:21;
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]:])
XBOOLE_0:def 10 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
object ;
TARSKI:def 3 ( 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:1;
assume
x in { p where p is Point of [:I[01],I[01]:] : p `2 <= (2 * (p `1)) - 1 }
;
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;
verum
end;
let x be
object ;
TARSKI:def 3 ( 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]:])
;
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;
verum
end;
x `2 <= (2 * (x `1)) - 1
;
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:13; verum