let h be non constant standard special_circular_sequence; :: thesis: for X being Subset of REAL st X = { (q `2) where q is Point of () : ( q `1 = E-bound (L~ h) & q in L~ h ) } holds
X = (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h)))

set T = () | (E-most (L~ h));
set F = proj2 | (E-most (L~ h));
let X be Subset of REAL; :: thesis: ( X = { (q `2) where q is Point of () : ( q `1 = E-bound (L~ h) & q in L~ h ) } implies X = (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h))) )
assume A1: X = { (q `2) where q is Point of () : ( q `1 = E-bound (L~ h) & q in L~ h ) } ; :: thesis: X = (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h)))
thus X c= (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h))) :: according to XBOOLE_0:def 10 :: thesis: (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h))) c= X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h))) )
A2: dom (proj2 | (E-most (L~ h))) = the carrier of (() | (E-most (L~ h))) by FUNCT_2:def 1
.= [#] (() | (E-most (L~ h)))
.= E-most (L~ h) by PRE_TOPC:def 5 ;
assume x in X ; :: thesis: x in (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h)))
then consider q1 being Point of () such that
A3: q1 `2 = x and
A4: q1 `1 = E-bound (L~ h) and
A5: q1 in L~ h by A1;
A6: x = (proj2 | (E-most (L~ h))) . q1 by ;
A7: q1 in E-most (L~ h) by ;
then q1 in the carrier of (() | (E-most (L~ h))) by ;
hence x in (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h))) by ; :: thesis: verum
end;
thus (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h))) c= X :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h))) or x in X )
A8: E-most (L~ h) c= L~ h by XBOOLE_1:17;
assume x in (proj2 | (E-most (L~ h))) .: the carrier of (() | (E-most (L~ h))) ; :: thesis: x in X
then consider x1 being object such that
x1 in dom (proj2 | (E-most (L~ h))) and
A9: x1 in the carrier of (() | (E-most (L~ h))) and
A10: x = (proj2 | (E-most (L~ h))) . x1 by FUNCT_1:def 6;
x1 in [#] (() | (E-most (L~ h))) by A9;
then A11: x1 in E-most (L~ h) by PRE_TOPC:def 5;
then reconsider x2 = x1 as Element of () ;
A12: x2 `1 = (E-min (L~ h)) `1 by
.= E-bound (L~ h) by EUCLID:52 ;
x = x2 `2 by ;
hence x in X by A1, A11, A12, A8; :: thesis: verum
end;