let X be Subset-Family of REAL ; :: thesis: ( card X in continuum implies ex x being real number ex q being rational number st
( x < q & not [.x,q.[ in UniCl X ) )
assume A1: card X in continuum ; :: thesis: ex x being real number ex q being rational number 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 ) } ;
consider z being 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_2:4;
then A3: ( z in REAL & not z 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 = z as Element of REAL by A2, XBOOLE_0:def 5;
z + 0 < z + 1 by XREAL_1:8;
then consider q being rational number such that
A4: ( z < q & q < z + 1 ) by RAT_1:22;
take z ; :: thesis: ex q being rational number 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 number 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:17; :: thesis: ].y,z.[ misses [.z,q.[
assume ].y,z.[ meets [.z,q.[ ; :: thesis: contradiction
then consider a being set such that
A5: ( a in ].y,z.[ & a in [.z,q.[ ) by XBOOLE_0:3;
reconsider a = a as Element of REAL by A5;
( a < z & z <= a ) by A5, XXREAL_1:3, XXREAL_1:4;
hence contradiction ; :: thesis: verum

end;

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