let I be set ; :: thesis: for Z, X, Y being ManySortedSet of I st Z c= X & Z c= Y holds
Z c= X /\ Y
let Z, X, Y be ManySortedSet of I; :: thesis: ( Z c= X & Z c= Y implies Z c= X /\ Y )
assume A1: ( Z c= X & Z c= Y ) ; :: thesis: Z c= X /\ Y
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( i in I implies Z . i c= (X /\ Y) . i )
assume A2: i in I ; :: thesis: Z . i c= (X /\ Y) . i
then ( Z . i c= X . i & Z . i c= Y . i ) by A1, Def5;
then Z . i c= (X . i) /\ (Y . i) by XBOOLE_1:19;
hence Z . i c= (X /\ Y) . i by A2, Def8; :: thesis: verum