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.[

( 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

hence
not [.z,q.[ in UniCl X
by A3; :: thesis: verum
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;( 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