for O being non empty RelStr st O is symmetric & O is transitive holds
O is SubReFlexive ;