lower_bound (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 5
.= the carrier of ((TOP-REAL 2) | (LSeg (|[0,1]|,|[1,1]|))) ;
A2: for p being Real st p in Z holds
p >= 0

proof

let p be Real; :: thesis: ( p in Z implies p >= 0 )
assume p in Z ; :: thesis: p >= 0
then consider p0 being object 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:64;
reconsider p0 = p0 as Point of (TOP-REAL 2) by A1, A3;
( |[0,1]| `1 = 0 & |[1,1]| `1 = 1 ) by EUCLID:52;
then p0 `1 >= 0 by A1, A3, TOPREAL1:3;
hence p >= 0 by A1, A3, A4, PSCOMP_1:22; :: thesis: verum

end;

for q being Real st ( for p being Real 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:22, RLTOPSP1:68
.= 0 by EUCLID:52 ;
A6: |[0,1]| in LSeg (|[0,1]|,|[1,1]|) by RLTOPSP1:68;
let q be Real; :: thesis: ( ( for p being Real st p in Z holds
p >= q ) implies 0 >= q )
assume for p being Real st p in Z holds
p >= q ; :: thesis: 0 >= q
hence 0 >= q by A1, A6, A5, FUNCT_2:35; :: thesis: verum

end;

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

end;

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