let I be set ; :: thesis: for f1, f2 being ManySortedSet of I st f1 c= f2 holds
Union f1 c= Union f2
let f1, f2 be ManySortedSet of I; :: thesis: ( f1 c= f2 implies Union f1 c= Union f2 )
assume A1: f1 c= f2 ; :: thesis: Union f1 c= Union f2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union f1 or x in Union f2 )
assume x in Union f1 ; :: thesis: x in Union f2
then consider y being object such that
A2: ( y in dom f1 & x in f1 . y ) by CARD_5:2;
A3: ( dom f1 = I & dom f2 = I ) by PARTFUN1:def 2;
f1 . y c= f2 . y by A1, A2;
hence x in Union f2 by A2, A3, CARD_5:2; :: thesis: verum