Step |
Hyp |
Ref |
Expression |
1 |
|
mopni.1 |
β’ π½ = ( MetOpen β π· ) |
2 |
|
blcld.3 |
β’ π = { π§ β π β£ ( π π· π§ ) β€ π
} |
3 |
1
|
mopnuni |
β’ ( π· β ( βMet β π ) β π = βͺ π½ ) |
4 |
3
|
3ad2ant1 |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β π = βͺ π½ ) |
5 |
4
|
difeq1d |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π β π ) = ( βͺ π½ β π ) ) |
6 |
|
difssd |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π β π ) β π ) |
7 |
|
simpl3 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β π
β β* ) |
8 |
|
simpl1 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β π· β ( βMet β π ) ) |
9 |
|
simpl2 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β π β π ) |
10 |
|
eldifi |
β’ ( π¦ β ( π β π ) β π¦ β π ) |
11 |
10
|
adantl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β π¦ β π ) |
12 |
|
xmetcl |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π¦ β π ) β ( π π· π¦ ) β β* ) |
13 |
8 9 11 12
|
syl3anc |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β ( π π· π¦ ) β β* ) |
14 |
|
eldif |
β’ ( π¦ β ( π β π ) β ( π¦ β π β§ Β¬ π¦ β π ) ) |
15 |
|
oveq2 |
β’ ( π§ = π¦ β ( π π· π§ ) = ( π π· π¦ ) ) |
16 |
15
|
breq1d |
β’ ( π§ = π¦ β ( ( π π· π§ ) β€ π
β ( π π· π¦ ) β€ π
) ) |
17 |
16 2
|
elrab2 |
β’ ( π¦ β π β ( π¦ β π β§ ( π π· π¦ ) β€ π
) ) |
18 |
17
|
simplbi2 |
β’ ( π¦ β π β ( ( π π· π¦ ) β€ π
β π¦ β π ) ) |
19 |
18
|
con3dimp |
β’ ( ( π¦ β π β§ Β¬ π¦ β π ) β Β¬ ( π π· π¦ ) β€ π
) |
20 |
14 19
|
sylbi |
β’ ( π¦ β ( π β π ) β Β¬ ( π π· π¦ ) β€ π
) |
21 |
20
|
adantl |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β Β¬ ( π π· π¦ ) β€ π
) |
22 |
|
xrltnle |
β’ ( ( π
β β* β§ ( π π· π¦ ) β β* ) β ( π
< ( π π· π¦ ) β Β¬ ( π π· π¦ ) β€ π
) ) |
23 |
7 13 22
|
syl2anc |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β ( π
< ( π π· π¦ ) β Β¬ ( π π· π¦ ) β€ π
) ) |
24 |
21 23
|
mpbird |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β π
< ( π π· π¦ ) ) |
25 |
|
qbtwnxr |
β’ ( ( π
β β* β§ ( π π· π¦ ) β β* β§ π
< ( π π· π¦ ) ) β β π₯ β β ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) |
26 |
7 13 24 25
|
syl3anc |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β β π₯ β β ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) |
27 |
|
qre |
β’ ( π₯ β β β π₯ β β ) |
28 |
8
|
adantr |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π· β ( βMet β π ) ) |
29 |
11
|
adantr |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π¦ β π ) |
30 |
13
|
adantr |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π π· π¦ ) β β* ) |
31 |
|
rexr |
β’ ( π₯ β β β π₯ β β* ) |
32 |
31
|
ad2antrl |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π₯ β β* ) |
33 |
32
|
xnegcld |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β -π π₯ β β* ) |
34 |
30 33
|
xaddcld |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( ( π π· π¦ ) +π -π π₯ ) β β* ) |
35 |
|
blelrn |
β’ ( ( π· β ( βMet β π ) β§ π¦ β π β§ ( ( π π· π¦ ) +π -π π₯ ) β β* ) β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ran ( ball β π· ) ) |
36 |
28 29 34 35
|
syl3anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ran ( ball β π· ) ) |
37 |
|
simprrr |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π₯ < ( π π· π¦ ) ) |
38 |
|
xposdif |
β’ ( ( π₯ β β* β§ ( π π· π¦ ) β β* ) β ( π₯ < ( π π· π¦ ) β 0 < ( ( π π· π¦ ) +π -π π₯ ) ) ) |
39 |
32 30 38
|
syl2anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π₯ < ( π π· π¦ ) β 0 < ( ( π π· π¦ ) +π -π π₯ ) ) ) |
40 |
37 39
|
mpbid |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β 0 < ( ( π π· π¦ ) +π -π π₯ ) ) |
41 |
|
xblcntr |
β’ ( ( π· β ( βMet β π ) β§ π¦ β π β§ ( ( ( π π· π¦ ) +π -π π₯ ) β β* β§ 0 < ( ( π π· π¦ ) +π -π π₯ ) ) ) β π¦ β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) ) |
42 |
28 29 34 40 41
|
syl112anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π¦ β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) ) |
43 |
|
incom |
β’ ( ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β© ( π ( ball β π· ) π₯ ) ) = ( ( π ( ball β π· ) π₯ ) β© ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) ) |
44 |
9
|
adantr |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π β π ) |
45 |
|
xaddcom |
β’ ( ( π₯ β β* β§ ( ( π π· π¦ ) +π -π π₯ ) β β* ) β ( π₯ +π ( ( π π· π¦ ) +π -π π₯ ) ) = ( ( ( π π· π¦ ) +π -π π₯ ) +π π₯ ) ) |
46 |
32 34 45
|
syl2anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π₯ +π ( ( π π· π¦ ) +π -π π₯ ) ) = ( ( ( π π· π¦ ) +π -π π₯ ) +π π₯ ) ) |
47 |
|
simprl |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π₯ β β ) |
48 |
|
xnpcan |
β’ ( ( ( π π· π¦ ) β β* β§ π₯ β β ) β ( ( ( π π· π¦ ) +π -π π₯ ) +π π₯ ) = ( π π· π¦ ) ) |
49 |
30 47 48
|
syl2anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( ( ( π π· π¦ ) +π -π π₯ ) +π π₯ ) = ( π π· π¦ ) ) |
50 |
46 49
|
eqtrd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π₯ +π ( ( π π· π¦ ) +π -π π₯ ) ) = ( π π· π¦ ) ) |
51 |
30
|
xrleidd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π π· π¦ ) β€ ( π π· π¦ ) ) |
52 |
50 51
|
eqbrtrd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π₯ +π ( ( π π· π¦ ) +π -π π₯ ) ) β€ ( π π· π¦ ) ) |
53 |
|
bldisj |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π¦ β π ) β§ ( π₯ β β* β§ ( ( π π· π¦ ) +π -π π₯ ) β β* β§ ( π₯ +π ( ( π π· π¦ ) +π -π π₯ ) ) β€ ( π π· π¦ ) ) ) β ( ( π ( ball β π· ) π₯ ) β© ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) ) = β
) |
54 |
28 44 29 32 34 52 53
|
syl33anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( ( π ( ball β π· ) π₯ ) β© ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) ) = β
) |
55 |
43 54
|
eqtrid |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β© ( π ( ball β π· ) π₯ ) ) = β
) |
56 |
|
blssm |
β’ ( ( π· β ( βMet β π ) β§ π¦ β π β§ ( ( π π· π¦ ) +π -π π₯ ) β β* ) β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β π ) |
57 |
28 29 34 56
|
syl3anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β π ) |
58 |
|
reldisj |
β’ ( ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β π β ( ( ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β© ( π ( ball β π· ) π₯ ) ) = β
β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π β ( π ( ball β π· ) π₯ ) ) ) ) |
59 |
57 58
|
syl |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( ( ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β© ( π ( ball β π· ) π₯ ) ) = β
β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π β ( π ( ball β π· ) π₯ ) ) ) ) |
60 |
55 59
|
mpbid |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π β ( π ( ball β π· ) π₯ ) ) ) |
61 |
7
|
adantr |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π
β β* ) |
62 |
|
simprrl |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π
< π₯ ) |
63 |
1 2
|
blsscls2 |
β’ ( ( ( π· β ( βMet β π ) β§ π β π ) β§ ( π
β β* β§ π₯ β β* β§ π
< π₯ ) ) β π β ( π ( ball β π· ) π₯ ) ) |
64 |
28 44 61 32 62 63
|
syl23anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β π β ( π ( ball β π· ) π₯ ) ) |
65 |
64
|
sscond |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π β ( π ( ball β π· ) π₯ ) ) β ( π β π ) ) |
66 |
60 65
|
sstrd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π β π ) ) |
67 |
|
eleq2 |
β’ ( π€ = ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π¦ β π€ β π¦ β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) ) ) |
68 |
|
sseq1 |
β’ ( π€ = ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π€ β ( π β π ) β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π β π ) ) ) |
69 |
67 68
|
anbi12d |
β’ ( π€ = ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( ( π¦ β π€ β§ π€ β ( π β π ) ) β ( π¦ β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β§ ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π β π ) ) ) ) |
70 |
69
|
rspcev |
β’ ( ( ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ran ( ball β π· ) β§ ( π¦ β ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β§ ( π¦ ( ball β π· ) ( ( π π· π¦ ) +π -π π₯ ) ) β ( π β π ) ) ) β β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) |
71 |
36 42 66 70
|
syl12anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ ( π₯ β β β§ ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) ) ) β β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) |
72 |
71
|
expr |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ π₯ β β ) β ( ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) β β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) ) |
73 |
27 72
|
sylan2 |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β§ π₯ β β ) β ( ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) β β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) ) |
74 |
73
|
rexlimdva |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β ( β π₯ β β ( π
< π₯ β§ π₯ < ( π π· π¦ ) ) β β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) ) |
75 |
26 74
|
mpd |
β’ ( ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β§ π¦ β ( π β π ) ) β β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) |
76 |
75
|
ralrimiva |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β β π¦ β ( π β π ) β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) |
77 |
1
|
elmopn |
β’ ( π· β ( βMet β π ) β ( ( π β π ) β π½ β ( ( π β π ) β π β§ β π¦ β ( π β π ) β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) ) ) |
78 |
77
|
3ad2ant1 |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( ( π β π ) β π½ β ( ( π β π ) β π β§ β π¦ β ( π β π ) β π€ β ran ( ball β π· ) ( π¦ β π€ β§ π€ β ( π β π ) ) ) ) ) |
79 |
6 76 78
|
mpbir2and |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π β π ) β π½ ) |
80 |
5 79
|
eqeltrrd |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( βͺ π½ β π ) β π½ ) |
81 |
1
|
mopntop |
β’ ( π· β ( βMet β π ) β π½ β Top ) |
82 |
81
|
3ad2ant1 |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β π½ β Top ) |
83 |
2
|
ssrab3 |
β’ π β π |
84 |
83 4
|
sseqtrid |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β π β βͺ π½ ) |
85 |
|
eqid |
β’ βͺ π½ = βͺ π½ |
86 |
85
|
iscld2 |
β’ ( ( π½ β Top β§ π β βͺ π½ ) β ( π β ( Clsd β π½ ) β ( βͺ π½ β π ) β π½ ) ) |
87 |
82 84 86
|
syl2anc |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β ( π β ( Clsd β π½ ) β ( βͺ π½ β π ) β π½ ) ) |
88 |
80 87
|
mpbird |
β’ ( ( π· β ( βMet β π ) β§ π β π β§ π
β β* ) β π β ( Clsd β π½ ) ) |