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

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