let A be Subset of R^1; :: thesis: for a, b, c being Real st a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds
Cl A = [.a,+infty.[
let a, b, c be Real; :: thesis: ( a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ implies Cl A = [.a,+infty.[ )
assume that
A1: a < b and
A2: b < c ; :: thesis: ( not A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ or Cl A = [.a,+infty.[ )
reconsider B = RAT (a,b) as Subset of R^1 by TOPMETR:17;
reconsider C = ].b,c.[ \/ ].c,+infty.[ as Subset of R^1 by TOPMETR:17;
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:20;
then Cl A = (Cl B) \/ [.b,+infty.[ by A2, Th54;
then Cl A = [.a,b.] \/ [.b,+infty.[ by A1, Th30;
hence Cl A = [.a,+infty.[ by A1, Th10; :: thesis: verum