Subset relation


THEOREM    $$A \subseteq B \Leftrightarrow (\forall x : x \in A \Rightarrow x \in B)$$
subset_iff: (?A \(\subseteq\) ?B) = (\(\forall\)t. t \(\in\) ?A \(\longrightarrow\) t \(\in\) ?B)

Proof unavailable

THEOREM   

The subset relation is reflexive.

$$A \subseteq A$$

Proof available

THEOREM   

The subset relation is antisymmetric.

Proof available

THEOREM   

The subset relation is transitive.

Proof available