nyuuzyou/wikis huggingface dataset:
Opposite Sides and Angles of Parallelogram are Equal

== Theorem ==
The opposite sides and angles of a parallelogram are equal to one another, and either of its diameters bisects its area.
== Proof ==
:
Let $ACDB$ be a parallelogram, and let $BC$ be a diameter.
By definition of parallelogram, $AB \parallel CD$, and $BC$ intersects both.
So by Parallelism implies Equal Alternate Angles:
:$\angle ABC = \angle BCD$
Similarly, by definition of parallelogram, $AC \parallel BD$, and $BC$ intersects both.
So by Parallelism implies Equal Alternate Angles:
:$\angle ACB = \angle CBD$
So $\triangle ABC$ and $\triangle DCB$ have two angles equal, and the side $BC$ in common.
So by Triangle Angle-Side-Angle Congruence:
: $\triangle ABC = \triangle DCB$
So $AC = BD$ and $AB = CD$.
Also, we have that $\angle BAC = \angle BDC$.
So we have $\angle ACB = \angle CBD$ and $\angle ABC = \angle BCD$.
So by :
:$\angle ACB + \angle BCD = \angle ABC + \angle CBD$
So $\angle ACD = \angle ABD$.
So we have shown that opposite sides and angles are equal to each other.
Now note that $AB = CD$, and $BC$ is common, and $\angle ABC = \angle BCD$.
So by Triangle Side-Angle-Side Congruence:
:$\triangle ABC = \triangle BCD$
So $BC$ bisects the parallelogram.
Similarly, $AD$ also bisects the parallelogram.
== Sources ==
* : Book $\text{I}$. Propositions
* : Chapter $1$: Triangles and Polygons: Theorems and Corollaries $1.22$
* 
Category:Parallelograms
Optimal Strategy for Fibonacci Nim

== Theorem ==
Consider a game of Fibonacci nim with $n$ counters.
Let it be the turn of player $\text A$.
Let the maximum number of counters that can be taken by $\text A$ be $q$.
Let $n$ be expressed in Zeckendorf representation as:
:$n = F_{k_1} + F_{k_2} + \cdots + F_{k_r}$
Then $\text A$ can force a win :
:$F_{k_r} \le q$
and by taking those $F_{k_r}$ counters.
== Proof ==
== Sources ==
* 
* : $\S 1.2.8$: Fibonacci Numbers: Exercise $37$
Category:Fibonacci Nim
Orbit-Stabilizer Theorem

== Theorem ==
Let $G$ be a group which acts on a finite set $X$.
Let $x \in X$.
Let $\Orb x$ denote the orbit of $x$.
Let $\Stab x$ denote the stabilizer of $x$ by $G$.
Let $\index G {\Stab x}$ denote the index of $\Stab x$ in $G$.
Then:
:$\order {\Orb x} = \index G {\Stab x} = \dfrac {\order G} {\order {\Stab x} }$
== Proof 1 ==
== Proof 2 ==
== Examples ==
Category:Group Actions
Category:Stabilizers
Category:Named Theorems
Category:Orbit-Stabilizer Theorem
Orbit-Stabilizer Theorem/Proof 1

== Theorem ==
== Proof ==
Let us define the mapping:
:$\phi: G \to \Orb x$
such that:
:$\map \phi g = g * x$
where $*$ denotes the group action.
It is clear that $\phi$ is surjective, because from the definition $x$ was acted on by all the elements of $G$.
Next, from Stabilizer is Subgroup: Corollary:
:$\map \phi g = \map \phi h \iff g^{-1} h \in \Stab x$
This means:
:$g \equiv h \pmod {\Stab x}$
Thus there is a well-defined bijection:
:$G \mathbin / \Stab x \to \Orb x$
given by:
:$g \, \Stab x \mapsto g * x$
So $\Orb x$ has the same number of elements as $G \mathbin / \Stab x$.
That is:
:$\order {\Orb x} = \index G {\Stab x}$
The result follows.
== Sources ==
* : Chapter $2$: The Sylow Theorems: $\S 54$
Category:Orbit-Stabilizer Theorem
Orbit-Stabilizer Theorem/Proof 2

== Theorem ==
== Proof ==
Let $x \in X$.
Let $\phi: \Orb x \to G \mathbin / \Stab x$ be a mapping from the orbit of $x$ to the left coset space of $\Stab x$ defined as:
:$\forall g \in G: \map \phi {g * x} = g \, \Stab x$
where $*$ is the group action.
Note: this is not a homomorphism because $\Orb x$ is not a group.
Suppose $g * x = h * x$ for some $g, h \in G$.
Then:
Thus:
:$h^{-1} g \in \Stab x$
so by Left Coset Space forms Partition:
:$g \, \Stab x = h \, \Stab x$
demonstrating that $\phi$ is well-defined.
Let $\map \phi {g_1 * x} = \map \phi {g_2 * x}$ for some $g_1, g_2 \in G$.
Then:
:$g_1 \, \Stab x = g_2 \, \Stab x$
and so by Left Coset Space forms Partition:
:$g_2^{-1} g_1 \in \Stab x$
So by definition of $\Stab x$:
:$x = \paren{g_2^{-1} g_1 }* x$
Thus:
thus demonstrating that $\phi$ is injective.
As the left coset $g \, \Stab x$ is $\map \phi {g * x}$ by definition of $\phi$, it follows that $\phi$ is a surjection.
The result follows.
== Sources ==
* : $\S 6.5$. Orbits
* : Chapter $10$: The Orbit-Stabiliser Theorem: Theorem $10.16$
Category:Orbit-Stabilizer Theorem
Orbit of Conjugacy Action on Subgroup is Set of Conjugate Subgroups

== Theorem ==
Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $X$ be the set of all subgroups of $G$.
Let $*$ be the conjugacy action on $H$ defined as:
: $\forall g \in G, H \in X: g * H = g \circ H \circ g^{-1}$
Then the orbit $\Orb H$ of $H$ in $\powerset G$ is the set of subgroups of $G$ conjugate to $H$.
== Proof ==
We have that:
:$\Orb H = \set {g \circ H \circ g^{-1}: g \in G}$
from the definition.
The result follows by definition of conjugate subgroup.
== Also see ==
* Conjugacy Action on Subgroups is Group Action
* Stabilizer of Conjugacy Action on Subgroup is Normalizer
== Sources ==
* : Chapter $10$: The Orbit-Stabiliser Theorem: Example $10.15$
Category:Conjugacy Action
Orbit of Dynamical System/Examples/Arbitrary Example 1

== Example of Orbit of Dynamical System ==
Let $T$ be the iterated mapping defined as:
:$\map T x = \dfrac x 2$
The orbit of $1$ under $T$ is the set $\set {1, \dfrac 1 2, \dfrac 1 4, \dfrac 1 8, \ldots}$
== Sources ==
* 
* 
Category:Examples of Orbits of Dynamical Systems
Orbit of Element of Group Acting on Itself is Group

== Theorem ==
Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $*$ be the group action of $\struct {G, \circ}$ on itself by the rule:
:$\forall g, h \in G: g * h = g \circ h$
Then the orbit of an element $x \in G$ is given by:
:$\Orb x = G$
== Proof ==
Let $y \in G$.
Then:
Hence the result.
== Also see ==
* Group Acts on Itself
* Stabilizer of Element of Group Acting on Itself is Trivial
== Sources ==
* : Chapter $10$: The Orbit-Stabiliser Theorem: Example $10.15$
Category:Group Actions
Orbit of Element under Conjugacy Action is Conjugacy Class

== Theorem ==
Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $*$ be the conjugacy group action on $G$:
: $\forall g, h \in G: g * h = g \circ h \circ g^{-1}$
Let $x \in G$.
Then the orbit of $x$ under this group action is:
:$\Orb x = C_x$
where $C_x$ is the conjugacy class of $x$.
== Proof ==
Follows from the definition of the conjugacy class.
== Also see ==
* Conjugacy Action on Group Elements is Group Action
* Stabilizer of Element under Conjugacy Action is Centralizer
== Sources ==
* : Chapter $10$: The Orbit-Stabiliser Theorem: Example $10.15$
Category:Conjugacy Action
Orbit of Group Action on Subgroup by Right Regular Representation is Right Coset

== Theorem ==
Let $G$ be a group.
Let $H$ be a proper subgroup of $G$.
Let $*: H \times G \to G$ be the group action defined as:
:$\forall \tuple {h, g} \in H \times G: h * g = \map {\rho_{h^{-1} } } g$
where $\map {\rho_{h^{-1} } } g$ is the right regular representation of $g$ by $h^{-1}$.
Let $x \in G$.
Then the orbit of $x$ under $*$ is given by:
:$\forall x \in G: \Orb x = H x$
where $H x$ is the right coset of $H$ by $x$.
== Proof ==
We are given $G$ is a group and $H$ is a proper subgroup of $G$, so:
:$H < G$
We are given $*: H \times G \to G$ is the group action defined as:
:$\forall \tuple {h, g} \in H \times G: h * g = \map {\rho_{h^{-1} } } g$
where $\map {\rho_{h^{-1} } } g$ is the right regular representation of $g$ by $h^{-1}$.
We are also given $x \in G$. 
So there exists $x \in G$ and $h \in H$ with $H < G$ such that:
:$h * x = \map {\rho_{h^{-1} } } x \in G$
Therefore the orbit of $x$ is given by:
:$\Orb x = \set {y \in G: \exists h \in H: y = h * x}$
Hence the result.
== Sources ==
* : $\S 3.3$: Group actions and coset decompositions
Category:Group Actions
Orbit of Subgroup Action is Coset

== Theorem ==
Let $\struct {G, \circ}$ be a group.
Let $\struct {H, \circ}$ be a subgroup of $G$.
Let $*: H \times G \to G$ be the subgroup action defined for all $h \in H, g \in G$ as:
:$\forall h \in H, g \in G: h * g := h \circ g$
The orbit of $x \in G$ is the right coset by $x$ of $H$:
:$\Orb x = H x$
== Proof ==
From Subgroup Action is Group Action we have that $*$ is a group action.
Let $x \in G$.
Then:
Hence the result, by definition of right coset.
== Sources ==
* : Chapter $6$: Cosets: Exercise $8$
* : Chapter $2$: The Sylow Theorems: $\S 54 \alpha$
Category:Subgroup Action
Orbit of Subgroup under Coset Action is Coset Space

== Theorem ==
Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\powerset G$ be the power set of $G$.
Let $H \in \powerset G$ be a subgroup of $G$.
Let $*$ be the group action on $H$ defined as:
:$\forall g \in G: g * H = g \circ H$
where $g \circ H$ is the (left) coset of $g$ by $H$.
Then the orbit of $H$ in $\powerset G$ is the (left) coset space of $H$:
:$\Orb H = G / H^l$
== Proof ==
From the definition of orbit:
:$\Orb H = \set {y \in G: \exists g \in G: y = g * H}$
By the definition of $*$:
:$\Orb H = \set {y \in G: \exists g \in G: y = g \circ H}$
The result follows from the definition of (left) coset space.
== Also see ==
* Subset Product Action is Group Action
* Stabilizer of Subset Product Action on Power Set
* Stabilizer of Coset Action on Set of Subgroups
== Sources ==
* : Chapter $10$: The Orbit-Stabiliser Theorem: Example $10.15$
Category:Subset Product Action
Orbit of Trivial Group Action is Singleton

== Theorem ==
Let $\left({G, \circ}\right)$ be a group whose identity is $e$.
Let $S$ be a set.
Let $*: G \times S \to S$ be the trivial group action:
:$\forall \left({g, s}\right) \in G \times S: g * s = s$
Let $s \in S$.
Then the orbit of $s$ under $*$ is $\left\{{s}\right\}$.
== Proof ==
By definition:
:$\operatorname{Orb} \left({s}\right) = \left\{{t \in S: \exists g \in G: g * s = t}\right\}$
By definition of the trivial group action:
:$\forall g \in G: g * s = s$
Hence the result.
== Sources ==
* : $\S 3.3$: Group actions and coset decompositions: Examples of group actions: $\text{(iii)}$
Category:Trivial Group Action
Orbits of Group Action on Sets with Power of Prime Size

== Lemma ==
Let $G$ be a finite group such that $\order G = k p^n$ where $p \nmid k$.
Let $\mathbb S = \set {S \subseteq G: \order S = p^n}$
Let $G$ act on $\mathbb S$ by the group action defined in Group Action on Sets with k Elements:
:$\forall S \in \mathbb S: g * S = g S = \set {x \in G: x = g s: s \in S}$
Then:
=== Orbit Length ===
=== Orbit whose Length is not Divisible by $p$ ===
=== Orbit whose Length is Divisible by $p$ ===
Category:Group Action on Prime Power Order Subset
Category:Orbits of Group Action on Sets with Power of Prime Size
Orbits of Group Action on Sets with Power of Prime Size/Orbit Length

== Lemma ==
Let $G$ be a finite group such that $\order G = k p^n$ where $p \nmid k$.
Let $\mathbb S = \set {S \subseteq G: \order S = p^n}$
Let $G$ act on $\mathbb S$ by the group action defined in Group Action on Sets with k Elements:
:$\forall S \in \mathbb S: g * S = g S = \set {x \in G: x = g s: s \in S}$
Then:
:The length of every orbit of this action is divisible by $k$.
== Proof ==
From the Orbit-Stabilizer Theorem, $\order G = \card {\Orb S} \times \order {\Stab S}$.
From Group Action on Prime Power Order Subset, $\Stab S$ is a $p$-subgroup of $G$.
Therefore:
:$k \nmid \order {\Stab S}$
and therefore:
:$k \divides \card {\Orb S}$
Category:Orbits of Group Action on Sets with Power of Prime Size
Orbits of Group Action on Sets with Power of Prime Size/Orbit whose Length is Divisible by p

== Lemma ==
Let $G$ be a finite group such that $\order G = k p^n$ where $p \nmid k$.
Let $\mathbb S = \set {S \subseteq G: \order S = p^n}$
Let $G$ act on $\mathbb S$ by the group action defined in Group Action on Sets with k Elements:
:$\forall S \in \mathbb S: g * S = g S = \set {x \in G: x = g s: s \in S}$
Then:
:Each orbit whose length is divisible by $p$ contains no Sylow $p$-subgroups.
== Proof ==
Let $H$ be a Sylow $p$-subgroup of $G$.
By the definition of $\mathbb S$, and because $\order H = p^n$:
:$H \in \mathbb S$
By Group Action on Sets with k Elements:
:$g \in G \implies g * H = g H$
which is a left coset of $G$.
However, we know that $g H = H \iff g \in H$.
Now:
:$g \in \Stab H \iff g * H = H \iff g \in H$
Thus:
:$\Stab H = H$
From the Orbit-Stabilizer Theorem:
:$\card {\Orb H} = k$
that is, not divisible by $p$.
As $H \in \Orb H$, the result follows.
Category:Orbits of Group Action on Sets with Power of Prime Size
Orbits of Group Action on Sets with Power of Prime Size/Orbit whose Length is not Divisible by p

== Lemma ==
Let $G$ be a finite group such that $\order G = k p^n$ where $p \nmid k$.
Let $\mathbb S = \set {S \subseteq G: \order S = p^n}$
Let $G$ act on $\mathbb S$ by the group action defined in Group Action on Sets with k Elements:
:$\forall S \in \mathbb S: g * S = g S = \set {x \in G: x = g s: s \in S}$
Then:
:Each orbit whose length is not divisible by $p$ contains exactly one Sylow $p$-subgroup.
== Proof ==
First it is shown that each orbit whose length is not divisible by $p$ contains at least one Sylow $p$-subgroup.
From the reasoning in the First Sylow Theorem, we know that:
:at least one $S \in \mathbb S$ is such that $p \nmid \card {\Orb S}$
and that for such a set:
:$\Stab S$ is a Sylow $p$-subgroup of $G$.
From Group Action on Prime Power Order Subset:
:$\forall s \in S: \Stab S s = S$
Therefore:
:$\Stab S = S s^{-1}$
Thus for any $s \in S$, $S s^{-1}$ is a Sylow $p$-subgroup of $G$.
It also follows that $s^{-1} \Stab S s$ is also a subgroup of $G$ with the same number of elements as $\Stab S$.
Thus $s^{-1} \Stab S s = s^{-1} \paren {S s^{-1} } s = s^{-1} S$ is a Sylow $p$-subgroup of $G$ in the orbit of $S$.
From the Orbit-Stabilizer Theorem:
:$\card {\Orb S} = k$
as $\order {\Stab S} = p^n$.
So if an orbit has length not divisible by $p$, this orbit contains at least one Sylow $p$-subgroup of $G$ (that is, $\Stab S$ and also $s^{-1} \Stab S s$).
The length of the orbit is $k$.
Next it is shown that each orbit whose length is not divisible by $p$ contains no more than one Sylow $p$-subgroup:
Let $H$ be a Sylow $p$-subgroup of $G$.
Now $\Orb H$ consists of all $g * H = g H$, that is, all the right cosets of $H$.
But the only right coset of $H$ which is a subgroup of $G$ is in fact $H$ itself.
None of the rest of the elements of $\mathbb S$ can actually be a subgroup of $G$.
Thus, no orbit can contain more than one Sylow $p$-subgroup.
Category:Orbits of Group Action on Sets with Power of Prime Size
Orchard Planting Problem

== Classic Problem ==
A given number $n$ of trees are to be planted in an orchard so as to make the number of rows of $k$ trees the largest number possible.
That is:
$n$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $k$ of these points is maximised.
=== Classic Form ===
== Solution ==
=== $12$ trees, $3$ in a row ===
== Also known as ==
The orchard planting problem can be seen hyphenated: orchard-planting problem.
It is also known as the orchard problem or tree-planting problem.
Note, however, that there exists another, completely different, orchard problem: the Orchard Visibility Problem, with which this one may be confused.
== Also see ==
* Orchard Visibility Problem
== Historical Note ==
== Sources ==
* 
* 
Category:Projective Geometry
Category:Discrete Geometry
Category:Recreational Mathematics
Category:Classic Problems
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form

== Classic Problem ==
A given number $n$ of trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$n$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
Let the maximum number of rows of $3$ for a given number of trees $n$ be denoted $t_3 \left({n}\right)$.
Then we have:
=== $3$ Trees ===
=== $4$ Trees ===
=== $5$ Trees ===
=== $6$ Trees ===
=== $7$ Trees ===
=== $8$ Trees ===
=== $9$ Trees ===
=== $10$ Trees ===
=== $11$ Trees ===
=== $12$ Trees ===
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/10

== Classic Problem ==
$10$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$10$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $12$.
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/11

== Classic Problem ==
$11$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$11$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $16$.
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/12

== Classic Problem ==
$12$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$12$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $19$.
$3$ of the points are at infinity.
One of the $19$ rows is also at infinity, and passes through each of those $3$ points.
== Sources ==
* 
* : $19$
Category:Orchard Planting Problem
Category:19
Orchard Planting Problem/Classic Form/3

== Classic Problem ==
$3$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$3$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $1$.
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/4

== Classic Problem ==
$4$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$4$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $1$.
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/5

== Classic Problem ==
$5$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$5$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $2$.
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/6

== Classic Problem ==
$6$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$6$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $4$.
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/7

== Classic Problem ==
$7$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$7$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $6$.
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/8

== Classic Problem ==
$8$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$8$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $7$.
Category:Orchard Planting Problem
Orchard Planting Problem/Classic Form/9

== Classic Problem ==
$9$ trees are to be planted in an orchard so as to make the number of rows of $3$ trees the largest number possible.
That is:
$9$ points are to be configured in the plane so that the number of straight lines that can be drawn through exactly $3$ of these points is maximised.
== Solution ==
:
The number of rows is $10$.
Category:Orchard Planting Problem
Orchard Planting Problem/Historical Note

== Historical Note on the Orchard Planting Problem ==
The Orchard Planting Problem appears to have first been set by in his $1821$ collection , where he worded it poetically as:
:1. Your aid I want, nine trees to plant
:::In rows just half a score;
::And let there be in each row three.
:::Solve this: I ask no more.
:2. Fain would I plant a grove in rows
::But how must I its form compose
:::With three trees in each row;
::To have as many rows as trees;
:::Now tell me, artists, if you please;
::'Tis all I want to know.
:3. Ingenious artists, if you please
:::To plant a grove, pray show,
::In twenty-three rows with fifteen trees
:::And three in every row.
:4. It is required to plant $17$ trees in $24$ rows,
and to have $3$ trees in every row.
:5. Ingenious artists, pray dispose
::Twenty-four trees in twenty-four rows.
::Three trees I'd have in every row;
::A pond in midst I'd have also.
::A plan thereof I fain would have,
::And therefore your assistance crave.
:6. Fam'd arborists, display your power
::And show how I may plant a bower
:::With verdant fir and yew:
::Twelve trees of each I would dispose,
::In only eight-and-twenty rows;
:::Four trees in each to view.
:7. Plant $27$ trees in $15$ rows, $5$ to a row.
:8. Ingenious artists, if you please,
::Now plant me five-and-twenty trees,
::In twenty-eight rows, nor less, nor more;
::In some rows five, some three, some four.
:9. It is required to plant $90$ trees in $10$ rows, with $10$ trees in each row; each tree equidistant from the other, also each row equidistant from a pond in the centre.
:10. A gentleman has a quadrangular irregular piece of ground, in which he is desirous of planting a quincunx, in such a manner, that all the rows of trees, whether transversal or diagonal, shall all be right lines. How must this be done?
:Note: A real quincunx is a plantation of trees disposed in a square, consisting of five trees, one at each corner, and the fifth in the middle; but in the present case, the trees are to be disposed in a quadrangle, one at each corner (as in the square), and the fifth at the point of intersection of the two diagonals.
== Sources ==
* 
Category:Historical Notes
Order-Extension Principle

== Theorem ==
Let $S$ be a set.
Let $\preceq$ be an ordering on $S$.
Then there exists a total ordering $\le$ on $S$ such that:
:$\forall a, b \in S: \paren {a \preceq b \implies a \le b}$
=== Strict Orderings ===
== Proof 1 ==
== Proof 2 ==
== Remarks ==
As shown in Proof 2, the order-extension principle is weaker than the Boolean Prime Ideal Theorem (BPI).
It is known that it is in fact strictly weaker than BPI.
However, it cannot be proved in Zermel-Fraenkel set theory without the .
In fact it is known to be strictly stronger than the Ordering Principle.
Category:Set Theory
Category:Order Theory
Category:Named Theorems
Category:Order-Extension Principle