# Meet in Inclusion Ordered Set

Jump to navigation
Jump to search

## Theorem

Let $P = \left({X, \subseteq}\right)$ be an inclusion ordered set.

Let $A, B \in X$ such that

- $A \cap B \in X$

Then $A \wedge B = A \cap B$

## Proof

- $A \cap B \subseteq A$ and $A \cap B \subseteq B$

By definition:

- $A \cap B$ is lower bound for $\left\{ {A, B}\right\}$

We will prove that

- $\forall C \in X: C$ is lower bound for $\left\{ {A, B}\right\} \implies C \subseteq A \cap B$

Let $C \in X$ such that

- $C$ is lower bound for $\left\{ {A, B}\right\}$.

By definition of lower bound:

- $C \subseteq A$ and $C \subseteq B$

Thus by Intersection is Largest Subset:

- $C \subseteq A \cap B$

$\Box$

By definition of infimum:

- $\inf \left\{ {A, B}\right\} = A \cap B$

Thus by definition of meet:

- $A \wedge B = A \cap B$

$\blacksquare$

## Sources

- Mizar article YELLOW_1:9