let I be set ; :: thesis: for X, Y, Z being ManySortedSet of st X meets Y & Y c= Z holds
X meets Z
let X, Y, Z be ManySortedSet of ; :: thesis: ( X meets Y & Y c= Z implies X meets Z )
assume that
A1: X meets Y and
A2: Y c= Z ; :: thesis: X meets Z
consider i being set such that
A3: ( i in I & X . i meets Y . i ) by A1, Def11;
take i ; :: according to PBOOLE:def 11 :: thesis: ( i in I & not X . i misses Z . i )
Y . i c= Z . i by A2, A3, Def5;
hence ( i in I & not X . i misses Z . i ) by A3, XBOOLE_1:63; :: thesis: verum