qed.
lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
∀R.
carrier_of_relation_class ? (relation_class_of_argument_class R) =
carrier_of_relation_class ? R.
qed.
lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
∀R.
carrier_of_relation_class ? (relation_class_of_argument_class R) =
carrier_of_relation_class ? R.