set X = R^2-unit_square ;
reconsider Z = (proj1 | R^2-unit_square ) .: the carrier of ((TOP-REAL 2) | R^2-unit_square ) as Subset of REAL ;
A1: R^2-unit_square = [#] ((TOP-REAL 2) | R^2-unit_square ) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | R^2-unit_square ) ;
A2: for p being real number st p in Z holds
p >= 0

proof

let p be real number ; :: thesis: ( p in Z implies p >= 0 )
assume p in Z ; :: thesis: p >= 0
then consider p0 being set such that
A3: p0 in the carrier of ((TOP-REAL 2) | R^2-unit_square ) and
p0 in the carrier of ((TOP-REAL 2) | R^2-unit_square ) and
A4: p = (proj1 | R^2-unit_square ) . p0 by FUNCT_2:115;
reconsider p0 = p0 as Point of (TOP-REAL 2) by A1, A3;
ex q being Point of (TOP-REAL 2) st
( p0 = q & ( ( q `1 = 0 & q `2 <= 1 & q `2 >= 0 ) or ( q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) or ( q `1 <= 1 & q `1 >= 0 & q `2 = 0 ) or ( q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) ) ) by A1, A3, TOPREAL1:20;
hence p >= 0 by A1, A3, A4, PSCOMP_1:69; :: thesis: verum

end;

for q being real number st ( for p being real number st p in Z holds
p >= q ) holds
0 >= q

proof

let q be real number ; :: thesis: ( ( for p being real number st p in Z holds
p >= q ) implies 0 >= q )
assume A5: for p being real number st p in Z holds
p >= q ; :: thesis: 0 >= q
|[0 ,0 ]| in LSeg |[0 ,0 ]|,|[1,0 ]| by RLTOPSP1:69;
then |[0 ,0 ]| in (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) by XBOOLE_0:def 3;
then A6: |[0 ,0 ]| in R^2-unit_square by XBOOLE_0:def 3;
then (proj1 | R^2-unit_square ) . |[0 ,0 ]| = |[0 ,0 ]| `1 by PSCOMP_1:69
.= 0 by EUCLID:56 ;
hence 0 >= q by A1, A5, A6, FUNCT_2:43; :: thesis: verum

end;

hence W-bound R^2-unit_square = 0 by A2, SEQ_4:61; :: thesis: verum