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 set st s in the carrier of R holds
not (ConstOSSet R,z) . s is empty by FUNCOP_1:13;
hence ConstOSSet R,z is non-empty by PBOOLE:def 16; :: 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 )
assume s1 <= s2 ; :: thesis: (ConstOSSet R,z) . s1 c= (ConstOSSet R,z) . s2
(the carrier of R --> z) . s1 = z by FUNCOP_1:13
.= (the carrier of R --> z) . s2 by FUNCOP_1:13 ;
hence (ConstOSSet R,z) . s1 c= (ConstOSSet R,z) . s2 ; :: thesis: verum