diff --git a/LeanByExample/Modifier/Private.lean b/LeanByExample/Modifier/Private.lean
index eb3a8eb3..b9c26b5c 100644
--- a/LeanByExample/Modifier/Private.lean
+++ b/LeanByExample/Modifier/Private.lean
@@ -1,20 +1,27 @@
 /- # private
-`private` は、その定義があるファイルの中でだけ参照可能になるようにする修飾子です。他のファイルからはアクセス不能になります。
+`private` は、その定義があるファイルの中でだけ参照可能になるようにする修飾子です。他のファイルからはアクセス不能になります。不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。
 
-不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。
+```admonish warning title="注意"
+このページの内容は <i class="fa fa-play"></i> ボタンから Lean 4 Web で実行することができません。
+```
+
+たとえば、以下のように書かれているファイル `PrivateLib.lean` があったとしましょう。
+
+{{#include ./PrivateLib.md}}
+
+このとき、モジュール `PrivateLib` を読み込んでいるファイルからは、`protected` で修飾された名前はアクセス可能ですが、`private` で修飾された名前はアクセスできません。
 -/
-import LeanByExample.Modifier.Protected -- protected のページをインポート
-import Lean
-namespace Private --#
+import LeanByExample.Modifier.PrivateLib -- private が使用されているモジュールをインポート
+import Lean --#
 
--- protected の項で private を使わずに定義した内容にアクセスできる
+-- private を使わずに定義した内容にはアクセスできる
 #check Point.sub
 
 -- private とマークした定義にはアクセスできない
 #guard_msgs (drop warning) in --#
 #check_failure Point.private_sub
 
-/- なお `private` コマンドで定義した名前は、そのセクションや名前空間を出てもアクセスすることができます。-/
+/- なお `private` コマンドで定義した名前は、同じファイル内であればそのセクションや名前空間を出てもアクセスすることができます。-/
 
 namespace Hoge
   section
@@ -29,7 +36,7 @@ open Hoge
 -- 外からでもアクセスできる
 #check addOne
 
-/- ## 補足
+/- ## 舞台裏
 `private` コマンドを用いて宣言した名前は、そのファイルの外部からはアクセス不能になるものの、そのファイル内部からは一見 `private` でない名前と同様に見えます。しかし、特定の名前が `private` であるか判定する関数は存在します。
 -/
 
@@ -43,5 +50,3 @@ def foo := "world"
 #guard Lean.isPrivateName ``hoge
 
 #guard Lean.isPrivateName ``foo = false
-
-end Private --#
diff --git a/LeanByExample/Modifier/PrivateLib.lean b/LeanByExample/Modifier/PrivateLib.lean
new file mode 100644
index 00000000..1772f379
--- /dev/null
+++ b/LeanByExample/Modifier/PrivateLib.lean
@@ -0,0 +1,14 @@
+-- PrivateLib.lean の内容
+
+structure Point where
+  x : Nat
+  y : Nat
+
+namespace Point
+
+protected def sub (p q : Point) : Point :=
+    { x := p.x - q.x, y := p.y - q.y }
+
+private def private_sub := Point.sub
+
+end Point
diff --git a/LeanByExample/Modifier/Protected.lean b/LeanByExample/Modifier/Protected.lean
index b1f5e8c2..33ac4f26 100644
--- a/LeanByExample/Modifier/Protected.lean
+++ b/LeanByExample/Modifier/Protected.lean
@@ -12,9 +12,6 @@ namespace Point
   protected def sub (p q : Point) : Point :=
     { x := p.x - q.x, y := p.y - q.y }
 
-  -- private のテスト用の宣言
-  private def private_sub := Point.sub
-
   -- 名前空間の中にいても、短い名前ではアクセスできない
   #guard_msgs (drop warning) in --#
   #check_failure sub