let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for u, v being Element of (NormForm A) st ( for c being Element of DISJOINT_PAIRS A st c in u holds
ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= c \/ a ) ) holds
ex b being Element of DISJOINT_PAIRS A st
( b in (@ u) =>> (@ v) & b c= a )
let a be Element of DISJOINT_PAIRS A; :: thesis: for u, v being Element of (NormForm A) st ( for c being Element of DISJOINT_PAIRS A st c in u holds
ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= c \/ a ) ) holds
ex b being Element of DISJOINT_PAIRS A st
( b in (@ u) =>> (@ v) & b c= a )
let u, v be Element of (NormForm A); :: thesis: ( ( for c being Element of DISJOINT_PAIRS A st c in u holds
ex b being Element of DISJOINT_PAIRS A st
( b in v & b c= c \/ a ) ) implies ex b being Element of DISJOINT_PAIRS A st
( b in (@ u) =>> (@ v) & b c= a ) )
defpred S₁[ Element of DISJOINT_PAIRS A, Element of [:(Fin A),(Fin A):]] means ( $2 in @ v & $2 c= $1 \/ a );
assume A1: for b being Element of DISJOINT_PAIRS A st b in u holds
ex c being Element of DISJOINT_PAIRS A st
( c in v & c c= b \/ a ) ; :: thesis: ex b being Element of DISJOINT_PAIRS A st
( b in (@ u) =>> (@ v) & b c= a )

A2: now :: thesis: for b being Element of DISJOINT_PAIRS A st b in @ u holds
ex x being Element of [:(Fin A),(Fin A):] st S₁[b,x]

let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in @ u implies ex x being Element of [:(Fin A),(Fin A):] st S₁[b,x] )
assume b in @ u ; :: thesis: ex x being Element of [:(Fin A),(Fin A):] st S₁[b,x]
then consider c being Element of DISJOINT_PAIRS A such that
A3: ( c in v & c c= b \/ a ) by A1;
reconsider c = c as Element of [:(Fin A),(Fin A):] ;
take x = c; :: thesis: S₁[b,x]
thus S₁[b,x] by A3; :: thesis: verum

end;

consider f9 being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) such that
A4: for b being Element of DISJOINT_PAIRS A st b in @ u holds
S₁[b,f9 . b] from FRAENKEL:sch 27(A2);
set d = FinPairUnion ((@ u),((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))));

A5: now :: thesis: for s being Element of DISJOINT_PAIRS A st s in u holds
((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s c= a

let s be Element of DISJOINT_PAIRS A; :: thesis: ( s in u implies ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s c= a )
assume s in u ; :: thesis: ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s c= a
then A6: f9 . s c= a \/ s by A4;
((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s = (f9 . s) \ s by Lm5;
hence ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) . s c= a by A6, NORMFORM:15; :: thesis: verum

end;

then reconsider d = FinPairUnion ((@ u),((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A))))) as Element of DISJOINT_PAIRS A by NORMFORM:21, NORMFORM:26;
take d ; :: thesis: ( d in (@ u) =>> (@ v) & d c= a )
for b being Element of DISJOINT_PAIRS A st b in u holds
f9 . b in v by A4;
then f9 .: (@ u) c= v by SETWISEO:10;
then d in { (FinPairUnion ((@ u),((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: (@ u) c= v } ;
hence d in (@ u) =>> (@ v) by XBOOLE_0:def 4; :: thesis: d c= a
thus d c= a by A5, NORMFORM:21; :: thesis: verum