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

proof

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

end;

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