theorem :: OPOSET_1:8

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