let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X meets Y & Y c= Z holds
X meets Z
let X, Y, Z be ManySortedSet of I; :: 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 object such that
A3: i in I and
A4: X . i meets Y . i by A1;
take i ; :: according to PBOOLE:def 8 :: thesis: ( i in I & not X . i misses Z . i )
Y . i c= Z . i by A2, A3;
hence ( i in I & not X . i misses Z . i ) by A3, A4, XBOOLE_1:63; :: thesis: verum