let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st Z c= X & Z c= Y holds
Z c= X (/\) Y
let X, Y, Z 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 object ; :: according to PBOOLE:def 2 :: 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;
then Z . i c= (X . i) /\ (Y . i) by XBOOLE_1:19;
hence Z . i c= (X (/\) Y) . i by A2, Def5; :: thesis: verum