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
proof
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;
thus (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X :: 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;