✐‹creator "Kevin Kappelmann"› theory LBinary_Relations imports Binary_Relations_Function Binary_Relations_Order Binary_Relation_Properties Binary_Relation_Functions Binary_Relations_Agree Binary_Relations_Extend Binary_Relations_Lattice Dependent_Binary_Relations Restricted_Equality Reverse_Implies begin paragraph ‹Summary› text ‹Basic concepts on binary relations.› end