✐‹creator "Kevin Kappelmann"› subsection ‹Basic Properties› theory Binary_Relation_Properties imports Binary_Relations_Antisymmetric Binary_Relations_Bi_Total Binary_Relations_Bi_Unique Binary_Relations_Connected Binary_Relations_Injective Binary_Relations_Irreflexive Binary_Relations_Left_Total Binary_Relations_Reflexive Binary_Relations_Right_Unique Binary_Relations_Surjective Binary_Relations_Symmetric Binary_Relations_Transitive begin end