let R be non empty Poset; :: thesis: for z being non empty set holds ConstOSSet R,z is order-sorted
let z be non empty set ; :: thesis: ConstOSSet R,z is order-sorted
set x = ConstOSSet R,z;
for s1, s2 being Element of R st s1 <= s2 holds
(ConstOSSet R,z) . s1 c= (ConstOSSet R,z) . s2 by Th15;
hence ConstOSSet R,z is order-sorted by Def18; :: thesis: verum