# Metamath Proof Explorer

## Theorem dedekindle

Description: The Dedekind cut theorem, with the hypothesis weakened to only require non-strict less than. (Contributed by Scott Fenton, 2-Jul-2013)

Ref Expression
Assertion dedekindle ${⊢}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)$

### Proof

Step Hyp Ref Expression
1 simpr1 ${⊢}\left({A}\cap {B}=\varnothing \wedge \left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\right)\to {A}\subseteq ℝ$
2 simpr2 ${⊢}\left({A}\cap {B}=\varnothing \wedge \left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\right)\to {B}\subseteq ℝ$
3 simp1 ${⊢}\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\to {A}\cap {B}=\varnothing$
4 simpl ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to {x}\in {A}$
5 disjel ${⊢}\left({A}\cap {B}=\varnothing \wedge {x}\in {A}\right)\to ¬{x}\in {B}$
6 3 4 5 syl2an ${⊢}\left(\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to ¬{x}\in {B}$
7 eleq1w ${⊢}{y}={x}\to \left({y}\in {B}↔{x}\in {B}\right)$
8 7 biimpcd ${⊢}{y}\in {B}\to \left({y}={x}\to {x}\in {B}\right)$
9 8 necon3bd ${⊢}{y}\in {B}\to \left(¬{x}\in {B}\to {y}\ne {x}\right)$
10 9 ad2antll ${⊢}\left(\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left(¬{x}\in {B}\to {y}\ne {x}\right)$
11 6 10 mpd ${⊢}\left(\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to {y}\ne {x}$
12 simp2 ${⊢}\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\to {A}\subseteq ℝ$
13 ssel2 ${⊢}\left({A}\subseteq ℝ\wedge {x}\in {A}\right)\to {x}\in ℝ$
14 12 4 13 syl2an ${⊢}\left(\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to {x}\in ℝ$
15 simp3 ${⊢}\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\to {B}\subseteq ℝ$
16 simpr ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to {y}\in {B}$
17 ssel2 ${⊢}\left({B}\subseteq ℝ\wedge {y}\in {B}\right)\to {y}\in ℝ$
18 15 16 17 syl2an ${⊢}\left(\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to {y}\in ℝ$
19 14 18 ltlend ${⊢}\left(\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left({x}<{y}↔\left({x}\le {y}\wedge {y}\ne {x}\right)\right)$
20 19 biimprd ${⊢}\left(\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left(\left({x}\le {y}\wedge {y}\ne {x}\right)\to {x}<{y}\right)$
21 11 20 mpan2d ${⊢}\left(\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left({x}\le {y}\to {x}<{y}\right)$
22 21 ralimdvva ${⊢}\left({A}\cap {B}=\varnothing \wedge {A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)$
23 22 3exp ${⊢}{A}\cap {B}=\varnothing \to \left({A}\subseteq ℝ\to \left({B}\subseteq ℝ\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\right)\right)$
24 23 3imp2 ${⊢}\left({A}\cap {B}=\varnothing \wedge \left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}<{y}$
25 dedekind ${⊢}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}<{y}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)$
26 1 2 24 25 syl3anc ${⊢}\left({A}\cap {B}=\varnothing \wedge \left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)$
27 26 ex ${⊢}{A}\cap {B}=\varnothing \to \left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)\right)$
28 n0 ${⊢}{A}\cap {B}\ne \varnothing ↔\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in \left({A}\cap {B}\right)$
29 simp1 ${⊢}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to {A}\subseteq ℝ$
30 elinel1 ${⊢}{w}\in \left({A}\cap {B}\right)\to {w}\in {A}$
31 ssel2 ${⊢}\left({A}\subseteq ℝ\wedge {w}\in {A}\right)\to {w}\in ℝ$
32 29 30 31 syl2an ${⊢}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge {w}\in \left({A}\cap {B}\right)\right)\to {w}\in ℝ$
33 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
34 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{B}\subseteq ℝ$
35 nfra1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
36 33 34 35 nf3an ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
37 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}\in \left({A}\cap {B}\right)$
38 36 37 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge {w}\in \left({A}\cap {B}\right)\right)$
39 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
40 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{B}\subseteq ℝ$
41 nfra2w ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
42 39 40 41 nf3an ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
43 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)$
44 42 43 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)$
45 rsp ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \left({x}\in {A}\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
46 elinel2 ${⊢}{w}\in \left({A}\cap {B}\right)\to {w}\in {B}$
47 breq2 ${⊢}{y}={w}\to \left({x}\le {y}↔{x}\le {w}\right)$
48 47 rspccv ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \left({w}\in {B}\to {x}\le {w}\right)$
49 46 48 syl5 ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \left({w}\in \left({A}\cap {B}\right)\to {x}\le {w}\right)$
50 45 49 syl6 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \left({x}\in {A}\to \left({w}\in \left({A}\cap {B}\right)\to {x}\le {w}\right)\right)$
51 50 com23 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\to \left({w}\in \left({A}\cap {B}\right)\to \left({x}\in {A}\to {x}\le {w}\right)\right)$
52 51 imp32 ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)\to {x}\le {w}$
53 52 3ad2antl3 ${⊢}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)\to {x}\le {w}$
54 53 adantr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)\wedge {y}\in {B}\right)\to {x}\le {w}$
55 simp3 ${⊢}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
56 30 adantr ${⊢}\left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\to {w}\in {A}$
57 breq1 ${⊢}{x}={w}\to \left({x}\le {y}↔{w}\le {y}\right)$
58 57 ralbidv ${⊢}{x}={w}\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\le {y}\right)$
59 58 rspccva ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\wedge {w}\in {A}\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\le {y}$
60 55 56 59 syl2an ${⊢}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{w}\le {y}$
61 60 r19.21bi ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)\wedge {y}\in {B}\right)\to {w}\le {y}$
62 54 61 jca ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)\wedge {y}\in {B}\right)\to \left({x}\le {w}\wedge {w}\le {y}\right)$
63 62 ex ${⊢}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)\to \left({y}\in {B}\to \left({x}\le {w}\wedge {w}\le {y}\right)\right)$
64 44 63 ralrimi ${⊢}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge \left({w}\in \left({A}\cap {B}\right)\wedge {x}\in {A}\right)\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {w}\wedge {w}\le {y}\right)$
65 64 expr ${⊢}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge {w}\in \left({A}\cap {B}\right)\right)\to \left({x}\in {A}\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {w}\wedge {w}\le {y}\right)\right)$
66 38 65 ralrimi ${⊢}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge {w}\in \left({A}\cap {B}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {w}\wedge {w}\le {y}\right)$
67 breq2 ${⊢}{z}={w}\to \left({x}\le {z}↔{x}\le {w}\right)$
68 breq1 ${⊢}{z}={w}\to \left({z}\le {y}↔{w}\le {y}\right)$
69 67 68 anbi12d ${⊢}{z}={w}\to \left(\left({x}\le {z}\wedge {z}\le {y}\right)↔\left({x}\le {w}\wedge {w}\le {y}\right)\right)$
70 69 2ralbidv ${⊢}{z}={w}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {w}\wedge {w}\le {y}\right)\right)$
71 70 rspcev ${⊢}\left({w}\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {w}\wedge {w}\le {y}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)$
72 32 66 71 syl2anc ${⊢}\left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge {w}\in \left({A}\cap {B}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)$
73 72 expcom ${⊢}{w}\in \left({A}\cap {B}\right)\to \left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)\right)$
74 73 exlimiv ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in \left({A}\cap {B}\right)\to \left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)\right)$
75 28 74 sylbi ${⊢}{A}\cap {B}\ne \varnothing \to \left(\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)\right)$
76 27 75 pm2.61ine ${⊢}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\le {z}\wedge {z}\le {y}\right)$