set GG = [:I[01] ,I[01] :];
set SS = [:R^1 ,R^1 :];
0 in the carrier of I[01]
by BORSUK_1:86;
then
[0 ,0 ] in [:the carrier of I[01] ,the carrier of I[01] :]
by ZFMISC_1:106;
then reconsider x = [0 ,0 ] as Point of [:I[01] ,I[01] :] by BORSUK_1:def 5;
( x `1 = 0 & x `2 = 0 )
by MCART_1:7;
then A1:
x `2 <= 1 - (2 * (x `1 ))
;
set P0 = { p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) } ;
A2:
x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) }
by A1;
reconsider PA = { p where p is Point of [:R^1 ,R^1 :] : p `2 <= 1 - (2 * (p `1 )) } as closed Subset of [:R^1 ,R^1 :] by Th25;
A3:
[:I[01] ,I[01] :] is SubSpace of [:R^1 ,R^1 :]
by BORSUK_3:25;
{ p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) } = PA /\ ([#] [:I[01] ,I[01] :])
proof
thus
{ p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `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 )) } 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 <= 1 - (2 * (p `1 )) } or x in PA /\ ([#] [:I[01] ,I[01] :]) )
assume
x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) }
;
:: thesis: x in PA /\ ([#] [:I[01] ,I[01] :])
then consider p being
Point of
[:I[01] ,I[01] :] such that A4:
(
x = p &
p `2 <= 1
- (2 * (p `1 )) )
;
A5:
x in the
carrier of
[:I[01] ,I[01] :]
by A4;
the
carrier of
[:I[01] ,I[01] :] c= the
carrier of
[:R^1 ,R^1 :]
by A3, BORSUK_1:35;
then reconsider a =
x as
Point of
[:R^1 ,R^1 :] by A5;
a `2 <= 1
- (2 * (a `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 <= 1 - (2 * (p `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 )) }
then
(
x in PA &
x in [#] [:I[01] ,I[01] :] )
by XBOOLE_0:def 4;
then
ex
p being
Point of
[:R^1 ,R^1 :] st
(
x = p &
p `2 <= 1
- (2 * (p `1 )) )
;
hence
x in { p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) }
by A6;
:: thesis: verum
end;
hence
{ p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) } is non empty closed Subset of [:I[01] ,I[01] :]
by A2, A3, PRE_TOPC:43; :: thesis: verum