inf (proj1 | (LSeg |[0 ,1]|,|[1,1]|)) = 0

proof

set X = LSeg |[0 ,1]|,|[1,1]|;
reconsider Z = (proj1 | (LSeg |[0 ,1]|,|[1,1]|)) .: the carrier of ((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|)) as Subset of REAL ;
A1: LSeg |[0 ,1]|,|[1,1]| = [#] ((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|)) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|)) ;
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) | (LSeg |[0 ,1]|,|[1,1]|)) and
p0 in the carrier of ((TOP-REAL 2) | (LSeg |[0 ,1]|,|[1,1]|)) and
A4: p = (proj1 | (LSeg |[0 ,1]|,|[1,1]|)) . p0 by FUNCT_2:115;
reconsider p0 = p0 as Point of (TOP-REAL 2) by A1, A3;
( |[0 ,1]| `1 = 0 & |[1,1]| `1 = 1 ) by EUCLID:56;
then p0 `1 >= 0 by A1, A3, TOPREAL1:9;
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

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

end;

hence inf (proj1 | (LSeg |[0 ,1]|,|[1,1]|)) = 0 by A2, SEQ_4:61; :: thesis: verum

end;

hence N-min R^2-unit_square = |[0 ,1]| by Th35, Th39; :: thesis: verum