let R be non empty Poset; :: thesis: for A being OrderSortedSet of R
for F being ManySortedFunction of the carrier of R st F is order-sorted holds
F .:.: A is OrderSortedSet of R
let A be OrderSortedSet of R; :: thesis: for F being ManySortedFunction of the carrier of R st F is order-sorted holds
F .:.: A is OrderSortedSet of R
let F be ManySortedFunction of the carrier of R; :: thesis: ( F is order-sorted implies F .:.: A is OrderSortedSet of R )
assume A1: F is order-sorted ; :: thesis: F .:.: A is OrderSortedSet of R
reconsider C1 = F .:.: A as ManySortedSet of R ;
C1 is order-sorted

proof

let s1, s2 be Element of R; :: according to OSALG_1:def 16 :: thesis: ( not s1 <= s2 or C1 . s1 c= C1 . s2 )
assume s1 <= s2 ; :: thesis: C1 . s1 c= C1 . s2
then A2: ( A . s1 c= A . s2 & F . s1 c= F . s2 ) by A1, Th1, OSALG_1:def 16;
( C1 . s1 = (F . s1) .: (A . s1) & C1 . s2 = (F . s2) .: (A . s2) ) by PBOOLE:def 20;
hence C1 . s1 c= C1 . s2 by A2, RELAT_1:125; :: thesis: verum

end;

hence F .:.: A is OrderSortedSet of R ; :: thesis: verum