let A be Subset of R^1 ; :: thesis: for a, b, c being real number st a < b & b < c & A = ((RAT a,b) \/ ].b,c.[) \/ ].c,+infty .[ holds
Cl A = [.a,+infty .[
let a, b, c be real number ; :: thesis: ( a < b & b < c & A = ((RAT a,b) \/ ].b,c.[) \/ ].c,+infty .[ implies Cl A = [.a,+infty .[ )
assume A1: ( a < b & b < c ) ; :: thesis: ( not A = ((RAT a,b) \/ ].b,c.[) \/ ].c,+infty .[ or Cl A = [.a,+infty .[ )
reconsider C = ].b,c.[ \/ ].c,+infty .[ as Subset of R^1 by TOPMETR:24;
reconsider B = RAT a,b as Subset of R^1 by TOPMETR:24;
assume A = ((RAT a,b) \/ ].b,c.[) \/ ].c,+infty .[ ; :: thesis: Cl A = [.a,+infty .[
then A = (RAT a,b) \/ C by XBOOLE_1:4;
then Cl A = (Cl B) \/ (Cl C) by PRE_TOPC:50;
then Cl A = (Cl B) \/ [.b,+infty .[ by A1, Th81;
then Cl A = [.a,b.] \/ [.b,+infty .[ by A1, Th54;
hence Cl A = [.a,+infty .[ by A1, Th28; :: thesis: verum