theorem Th43: :: ORDERS_5:34

for A being non empty Preorder
for x being Element of A holds Class ((EqRelOf A),x) in the carrier of (QuotientOrder A)