let I be set ; :: thesis: for A, X being ManySortedSet of I holds
( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
let A, X be ManySortedSet of I; :: thesis: ( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
thus ( A in union X implies ex Y being ManySortedSet of I st
( A in Y & Y in X ) ) :: thesis: ( ex Y being ManySortedSet of I st
( A in Y & Y in X ) implies A in union X )

proof

defpred S₁[ set , set ] means ( A . $1 in $2 & $2 in X . $1 );
assume A1: A in union X ; :: thesis: ex Y being ManySortedSet of I st
( A in Y & Y in X )
A2: for i being set st i in I holds
ex Y being set st S₁[i,Y]

proof

let i be set ; :: thesis: ( i in I implies ex Y being set st S₁[i,Y] )
assume A3: i in I ; :: thesis: ex Y being set st S₁[i,Y]
then A . i in (union X) . i by A1, PBOOLE:def 1;
then A . i in union (X . i) by A3, Def2;
hence ex Y being set st S₁[i,Y] by TARSKI:def 4; :: thesis: verum

end;

consider K being ManySortedSet of I such that
A4: for i being set st i in I holds
S₁[i,K . i] from PBOOLE:sch 3(A2);
take K ; :: thesis: ( A in K & K in X )
thus A in K :: thesis: K in X

proof

let i be set ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in K . i )
assume i in I ; :: thesis: A . i in K . i
hence A . i in K . i by A4; :: thesis: verum

end;

thus K in X :: thesis: verum

proof

let i be set ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or K . i in X . i )
assume i in I ; :: thesis: K . i in X . i
hence K . i in X . i by A4; :: thesis: verum

end;

end;

given Y being ManySortedSet of I such that A5: ( A in Y & Y in X ) ; :: thesis: A in union X
let i be set ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in (union X) . i )
assume A6: i in I ; :: thesis: A . i in (union X) . i
then ( A . i in Y . i & Y . i in X . i ) by A5, PBOOLE:def 1;
then A . i in union (X . i) by TARSKI:def 4;
hence A . i in (union X) . i by A6, Def2; :: thesis: verum