let h be non constant standard special_circular_sequence; 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; ( 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 ) }
; 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)))
XBOOLE_0:def 10 (proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= Xproof
let x be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
thus
(proj2 | (W-most (L~ h))) .: the carrier of ((TOP-REAL 2) | (W-most (L~ h))) c= X
verum