let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for u, v being Element of () 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 () 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 (); :: 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 S1[ 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 S1[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 S1[b,x] )
assume b in @ u ; :: thesis: ex x being Element of [:(Fin A),(Fin A):] st S1[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: S1[b,x]
thus S1[b,x] by A3; :: thesis: verum
end;
consider f9 being Element of Funcs ((),[:(Fin A),(Fin A):]) such that
A4: for b being Element of DISJOINT_PAIRS A st b in @ u holds
S1[b,f9 . b] from set d = FinPairUnion ((@ u),(() .: (f9,())));
A5: now :: thesis: for s being Element of DISJOINT_PAIRS A st s in u holds
(() .: (f9,())) . s c= a
let s be Element of DISJOINT_PAIRS A; :: thesis: ( s in u implies (() .: (f9,())) . s c= a )
assume s in u ; :: thesis: (() .: (f9,())) . s c= a
then A6: f9 . s c= a \/ s by A4;
((pair_diff A) .: (f9,())) . s = (f9 . s) \ s by Lm5;
hence ((pair_diff A) .: (f9,())) . s c= a by ; :: thesis: verum
end;
then reconsider d = FinPairUnion ((@ u),(() .: (f9,()))) as Element of DISJOINT_PAIRS A by ;
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),(() .: (f,())))) where f is Element of Funcs ((),[:(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 ; :: thesis: verum