let R be non empty Poset; :: thesis: for X, Y being OrderSortedSet of R holds X (/\) Y is OrderSortedSet of R
let X, Y be OrderSortedSet of R; :: thesis: X (/\) Y is OrderSortedSet of R
reconsider M = X (/\) Y as ManySortedSet of R ;
M is order-sorted

proof

let s1, s2 be Element of R; :: according to OSALG_1:def 16 :: thesis: ( not s1 <= s2 or M . s1 c= M . s2 )
assume s1 <= s2 ; :: thesis: M . s1 c= M . s2
then A1: ( X . s1 c= X . s2 & Y . s1 c= Y . s2 ) by OSALG_1:def 16;
( (X (/\) Y) . s1 = (X . s1) /\ (Y . s1) & (X (/\) Y) . s2 = (X . s2) /\ (Y . s2) ) by PBOOLE:def 5;
hence M . s1 c= M . s2 by A1, XBOOLE_1:27; :: thesis: verum

end;

hence X (/\) Y is OrderSortedSet of R ; :: thesis: verum