theorem Th15: :: OSALG_1:15

for R being non empty Poset
for z being non empty set holds
( ConstOSSet (R,z) is non-empty & ( for s1, s2 being Element of R st s1 <= s2 holds
(ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2 ) )