let X be Subset-Family of REAL; ( card X in continuum implies ex x being Real ex q being Rational st
( x < q & not [.x,q.[ in UniCl X ) )
assume A1:
card X in continuum
; ex x being Real ex q being Rational st
( x < q & not [.x,q.[ in UniCl X )
set Z = { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } ;
set z = the Element of REAL \ { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } ;
card { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } in continuum
by A1, Th31;
then A2:
REAL \ { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } <> {}
by CARD_1:68;
then A3:
not the Element of REAL \ { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } in { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) }
by XBOOLE_0:def 5;
reconsider z = the Element of REAL \ { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } as Element of REAL by A2, XBOOLE_0:def 5;
z + 0 < z + 1
by XREAL_1:6;
then consider q being Rational such that
A4:
z < q
and
q < z + 1
by RAT_1:7;
take
z
; ex q being Rational st
( z < q & not [.z,q.[ in UniCl X )
take
q
; ( z < q & not [.z,q.[ in UniCl X )
thus
z < q
by A4; not [.z,q.[ in UniCl X
z is_local_minimum_of [.z,q.[
proof
thus
z in [.z,q.[
by A4, XXREAL_1:3;
TOPGEN_3:def 3 ex y being Real st
( y < z & ].y,z.[ misses [.z,q.[ )
take y =
z - 1;
( y < z & ].y,z.[ misses [.z,q.[ )
z - 0 = z
;
hence
y < z
by XREAL_1:15;
].y,z.[ misses [.z,q.[
assume
].y,z.[ meets [.z,q.[
;
contradiction
then consider a being
object such that A5:
a in ].y,z.[
and A6:
a in [.z,q.[
by XBOOLE_0:3;
reconsider a =
a as
Element of
REAL by A5;
a < z
by A5, XXREAL_1:4;
hence
contradiction
by A6, XXREAL_1:3;
verum
end;
hence
not [.z,q.[ in UniCl X
by A3; verum