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

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

hence
F .:.: A is OrderSortedSet of R
; :: thesis: verum
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;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