List of theorems in general/Relations_2.gh:

(→ (∧ (= A (orderedPair b c)) (∧ (∈ b B) (∈ c C))) (= (1st A) b))

(→ (∧ (= A (orderedPair b c)) (∧ (∈ b B) (∈ c C))) (∈ (1st A) B))

(→ (∧ (= A (orderedPair b c)) (∧ (∈ b B) (∈ c C))) (= (2nd A) c))

(→ (∧ (= A (orderedPair b c)) (∧ (∈ b B) (∈ c C))) (∈ (2nd A) C))

(→ (∈ A (× B C)) (∧ (∈ (1st A) B) (∈ (2nd A) C)))