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 (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } holds

X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))

set T = (TOP-REAL 2) | (W-most (L~ h));

set F = proj2 | (W-most (L~ h));

let X be Subset of REAL; :: thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } implies X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) )

assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } ; :: thesis: X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))

thus X c= (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) :: according to XBOOLE_0:def 10 :: thesis: (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X

X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))

set T = (TOP-REAL 2) | (W-most (L~ h));

set F = proj2 | (W-most (L~ h));

let X be Subset of REAL; :: thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } implies X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) )

assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : ( q `1 = W-bound (L~ h) & q in L~ h ) } ; :: thesis: X = (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))

thus X c= (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) :: according to XBOOLE_0:def 10 :: thesis: (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X

proof

thus
(proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) )

A2: dom (proj2 | (W-most (L~ h))) = the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by FUNCT_2:def 1

.= [#] ((TOP-REAL 2) | (W-most (L~ h)))

.= W-most (L~ h) by PRE_TOPC:def 5 ;

assume x in X ; :: thesis: x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))

then consider q1 being Point of (TOP-REAL 2) such that

A3: q1 `2 = x and

A4: q1 `1 = W-bound (L~ h) and

A5: q1 in L~ h by A1;

A6: x = (proj2 | (W-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:23, SPRECT_2:12;

A7: q1 in W-most (L~ h) by A4, A5, SPRECT_2:12;

then q1 in the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by A2, FUNCT_2:def 1;

hence x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by A2, A7, A6, FUNCT_1:def 6; :: thesis: verum

end;A2: dom (proj2 | (W-most (L~ h))) = the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by FUNCT_2:def 1

.= [#] ((TOP-REAL 2) | (W-most (L~ h)))

.= W-most (L~ h) by PRE_TOPC:def 5 ;

assume x in X ; :: thesis: x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h)))

then consider q1 being Point of (TOP-REAL 2) such that

A3: q1 `2 = x and

A4: q1 `1 = W-bound (L~ h) and

A5: q1 in L~ h by A1;

A6: x = (proj2 | (W-most (L~ h))) . q1 by A3, A4, A5, PSCOMP_1:23, SPRECT_2:12;

A7: q1 in W-most (L~ h) by A4, A5, SPRECT_2:12;

then q1 in the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by A2, FUNCT_2:def 1;

hence x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) by A2, A7, A6, FUNCT_1:def 6; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) or x in X )

A8: W-most (L~ h) c= L~ h by XBOOLE_1:17;

assume x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) ; :: thesis: x in X

then consider x1 being object such that

x1 in dom (proj2 | (W-most (L~ h))) and

A9: x1 in the carrier of ((TOP-REAL 2) | (W-most (L~ h))) and

A10: x = (proj2 | (W-most (L~ h))) . x1 by FUNCT_1:def 6;

x1 in [#] ((TOP-REAL 2) | (W-most (L~ h))) by A9;

then A11: x1 in W-most (L~ h) by PRE_TOPC:def 5;

then reconsider x2 = x1 as Element of (TOP-REAL 2) ;

A12: x2 `1 = (W-min (L~ h)) `1 by A11, PSCOMP_1:31

.= W-bound (L~ h) by EUCLID:52 ;

x = x2 `2 by A10, A11, PSCOMP_1:23;

hence x in X by A1, A11, A12, A8; :: thesis: verum

end;A8: W-most (L~ h) c= L~ h by XBOOLE_1:17;

assume x in (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) ; :: thesis: x in X

then consider x1 being object such that

x1 in dom (proj2 | (W-most (L~ h))) and

A9: x1 in the carrier of ((TOP-REAL 2) | (W-most (L~ h))) and

A10: x = (proj2 | (W-most (L~ h))) . x1 by FUNCT_1:def 6;

x1 in [#] ((TOP-REAL 2) | (W-most (L~ h))) by A9;

then A11: x1 in W-most (L~ h) by PRE_TOPC:def 5;

then reconsider x2 = x1 as Element of (TOP-REAL 2) ;

A12: x2 `1 = (W-min (L~ h)) `1 by A11, PSCOMP_1:31

.= W-bound (L~ h) by EUCLID:52 ;

x = x2 `2 by A10, A11, PSCOMP_1:23;

hence x in X by A1, A11, A12, A8; :: thesis: verum