Theorem empty_relation

Proof
01. ⊢ ∅ ⊆ X × Y, empty_set_is_least.
empty_relation. ⊢ relation ∅, relation_from_incl 1.

Dependencies
The given proof depends on three axioms:
comp, efq, eq_subst.