let R be non empty Poset; :: thesis: 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 ) )
let z be non empty set ; :: thesis: ( 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 ) )
set x = ConstOSSet (R,z);
set D = the carrier of R --> z;
for s being object st s in the carrier of R holds
not (ConstOSSet (R,z)) . s is empty by FUNCOP_1:7;
hence ConstOSSet (R,z) is non-empty by PBOOLE:def 13; :: thesis: for s1, s2 being Element of R st s1 <= s2 holds
(ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2
let s1, s2 be Element of R; :: thesis: ( s1 <= s2 implies (ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2 )
( the carrier of R --> z) . s1 = z by FUNCOP_1:7
.= ( the carrier of R --> z) . s2 by FUNCOP_1:7 ;
hence ( s1 <= s2 implies (ConstOSSet (R,z)) . s1 c= (ConstOSSet (R,z)) . s2 ) ; :: thesis: verum