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₁[ object , object ] means ex B being set st
( B = $2 & A . $1 in B & $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 object st i in I holds
ex Y being object st S₁[i,Y]

proof

let i be object ; :: thesis: ( i in I implies ex Y being object st S₁[i,Y] )
assume A3: i in I ; :: thesis: ex Y being object st S₁[i,Y]
then A . i in (union X) . i by A1;
then A . i in union (X . i) by A3, Def2;
then consider B being set such that
A4: ( A . i in B & B in X . i ) by TARSKI:def 4;
take B ; :: thesis: S₁[i,B]
thus S₁[i,B] by A4; :: thesis: verum

end;

consider K being ManySortedSet of I such that
A5: for i being object 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 object ; :: 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
then S₁[i,K . i] by A5;
hence A . i in K . i ; :: thesis: verum

end;

thus K in X :: thesis: verum

proof

let i be object ; :: 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
then S₁[i,K . i] by A5;
hence K . i in X . i ; :: thesis: verum

end;

end;

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