let A be Subset of R^1; 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; ( 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
; ( 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.[
; 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; verum