let a be Point of (TOP-REAL 2); :: thesis: proj1 .: (west_halfline a) is bounded_above
take a `1 ; :: according to SEQ_4:def 1 :: thesis: for b<sub>1</sub> being set holds
( not b<sub>1</sub> in proj1 .: (west_halfline a) or b<sub>1</sub> <= a `1 )
let r be real number ; :: 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 set 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:115;
reconsider x = x as Point of (TOP-REAL 2) by A1;
r = x `1 by A3, PSCOMP_1:def 28;
hence r <= a `1 by A2, TOPREAL1:def 15; :: thesis: verum