defpred S₁[ object ] means ex a, y being set st
( $1 = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) );
consider T being set such that
A1: for x being object holds
( x in T iff ( x in [:(dom f),(Union f):] & S₁[x] ) ) from XBOOLE_0:sch 1();
take T ; :: thesis: for x being set holds
( x in T iff ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) )
let x be set ; :: thesis: ( x in T iff ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) )

now :: thesis: ( ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) implies x in [:(dom f),(Union f):] )

given a, y being set such that A2: x = [a,y] and
A3: a in dom f and
A4: y in f . a and
for b being set st b in dom f & b c= a & y in f . b holds
a = b ; :: thesis: x in [:(dom f),(Union f):]
y in Union f by A3, A4, CARD_5:2;
hence x in [:(dom f),(Union f):] by A2, A3, ZFMISC_1:87; :: thesis: verum

end;

hence ( x in T iff ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) ) by A1; :: thesis: verum