let a be Point of (TOP-REAL 2); :: thesis: proj1 .: (west_halfline a) is bounded_above

take a `1 ; :: according to XXREAL_2:def 10 :: thesis: a `1 is UpperBound of proj1 .: (west_halfline a)

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in proj1 .: (west_halfline a) or r <= a `1 )

assume r in proj1 .: (west_halfline a) ; :: thesis: r <= a `1

then consider x being object such that

A1: x in the carrier of (TOP-REAL 2) and

A2: x in west_halfline a and

A3: r = proj1 . x by FUNCT_2:64;

reconsider x = x as Point of (TOP-REAL 2) by A1;

r = x `1 by A3, PSCOMP_1:def 5;

hence r <= a `1 by A2, TOPREAL1:def 13; :: thesis: verum

take a `1 ; :: according to XXREAL_2:def 10 :: thesis: a `1 is UpperBound of proj1 .: (west_halfline a)

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in proj1 .: (west_halfline a) or r <= a `1 )

assume r in proj1 .: (west_halfline a) ; :: thesis: r <= a `1

then consider x being object such that

A1: x in the carrier of (TOP-REAL 2) and

A2: x in west_halfline a and

A3: r = proj1 . x by FUNCT_2:64;

reconsider x = x as Point of (TOP-REAL 2) by A1;

r = x `1 by A3, PSCOMP_1:def 5;

hence r <= a `1 by A2, TOPREAL1:def 13; :: thesis: verum