let X be Subset-Family of REAL; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex q being Rational st
( z < q & not [.z,q.[ in UniCl X )
take q ; :: thesis: ( z < q & not [.z,q.[ in UniCl X )
thus z < q by A4; :: thesis: not [.z,q.[ in UniCl X
z is_local_minimum_of [.z,q.[

proof

thus z in [.z,q.[ by A4, XXREAL_1:3; :: according to TOPGEN_3:def 3 :: thesis: ex y being Real st
( y < z & ].y,z.[ misses [.z,q.[ )
take y = z - 1; :: thesis: ( y < z & ].y,z.[ misses [.z,q.[ )
z - 0 = z ;
hence y < z by XREAL_1:15; :: thesis: ].y,z.[ misses [.z,q.[
assume ].y,z.[ meets [.z,q.[ ; :: thesis: 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; :: thesis: verum

end;

hence not [.z,q.[ in UniCl X by A3; :: thesis: verum