let A be non empty Preorder; :: thesis: for x being Element of A holds Class ((EqRelOf A),x) in the carrier of (QuotientOrder A)
let x be Element of A; :: thesis: Class ((EqRelOf A),x) in the carrier of (QuotientOrder A)
Class ((EqRelOf A),x) in Class (EqRelOf A) by EQREL_1:def 3;
hence Class ((EqRelOf A),x) in the carrier of (QuotientOrder A) by Def7; :: thesis: verum