Binary Relations

• Reflexive: ∀x:x~x
• Irreflexive: ∀x:x≁x
• Symmetric: ∀xy:x~y→y~x
• Antisymmetric: ∀xy:(x≠y∧x~y)→y~x
• Asymmetric: ∀xy:x~y→y≁x
• Transitive: ∀xyz:(x≁y∧y≁z)→x~z
• Total: ∀xy:x~y∨y~x
• Well-founded: ∀S≠∅ ∃m∈S ∀x∈S: s≁m, where S is a nonempty subset
• Has joins: ∀xy∃s: s~x ∧ s~y ∧ [∀w:(s~x∧s~y)→w~s]
• Has meets: ∀xy∃s: x~s ∧ y~s ∧ [∀w:(x~s∧y~s)→s~w]

	Reflexive	Irreflexive	Symmetric	Antisymmetric	Asymmetric	Transitive	Total	Well-founded	Has joins	Has meets