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