theorem Th11: :: OPOSET_1:11

for O being non empty RelStr st O is QuasiOrdered holds
O is SubQuasiOrdered