let h be non constant standard special_circular_sequence; :: thesis: for X being Subset of REAL st X = { (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } holds
X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h)))
set T = (TOP-REAL 2) | (N-most (L~ h));
set F = proj1 | (N-most (L~ h));
let X be Subset of REAL ; :: thesis: ( X = { (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } implies X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) )
assume A1: X = { (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ h) & q in L~ h ) } ; :: thesis: X = (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h)))
thus X c= (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) :: according to XBOOLE_0:def 10 :: thesis: (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) )
assume x in X ; :: thesis: x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h)))
then consider q1 being Point of (TOP-REAL 2) such that
A2: ( q1 `1 = x & q1 `2 = N-bound (L~ h) & q1 in L~ h ) by A1;
A3: dom (proj1 | (N-most (L~ h))) = the carrier of ((TOP-REAL 2) | (N-most (L~ h))) by FUNCT_2:def 1
.= [#] ((TOP-REAL 2) | (N-most (L~ h)))
.= N-most (L~ h) by PRE_TOPC:def 10 ;
q1 in N-most (L~ h) by A2, SPRECT_2:14;
then ( q1 in dom (proj1 | (N-most (L~ h))) & q1 in the carrier of ((TOP-REAL 2) | (N-most (L~ h))) & x = (proj1 | (N-most (L~ h))) . q1 ) by A2, A3, FUNCT_2:def 1, PSCOMP_1:69;
hence x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) by FUNCT_1:def 12; :: thesis: verum

end;

thus (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) c= X :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) or x in X )
assume x in (proj1 | (N-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (N-most (L~ h))) ; :: thesis: x in X
then consider x1 being set such that
A4: ( x1 in dom (proj1 | (N-most (L~ h))) & x1 in the carrier of ((TOP-REAL 2) | (N-most (L~ h))) & x = (proj1 | (N-most (L~ h))) . x1 ) by FUNCT_1:def 12;
x1 in [#] ((TOP-REAL 2) | (N-most (L~ h))) by A4;
then A5: x1 in N-most (L~ h) by PRE_TOPC:def 10;
then reconsider x2 = x1 as Element of (TOP-REAL 2) ;
A6: x = x2 `1 by A4, A5, PSCOMP_1:69;
A7: x2 `2 = (N-min (L~ h)) `2 by A5, PSCOMP_1:98
.= N-bound (L~ h) by EUCLID:56 ;
N-most (L~ h) c= L~ h by XBOOLE_1:17;
hence x in X by A1, A5, A6, A7; :: thesis: verum

end;