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_{1}[ 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 )

A4: for b being Element of DISJOINT_PAIRS A st b in @ u holds

S_{1}[b,f9 . b]
from FRAENKEL:sch 27(A2);

set d = FinPairUnion ((@ u),((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))));

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

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

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_{1}[b,x]

consider f9 being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) such that ex x being Element of [:(Fin A),(Fin A):] st S

let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in @ u implies ex x being Element of [:(Fin A),(Fin A):] st S_{1}[b,x] )

assume b in @ u ; :: thesis: ex x being Element of [:(Fin A),(Fin A):] st S_{1}[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_{1}[b,x]

thus S_{1}[b,x]
by A3; :: thesis: verum

end;assume b in @ u ; :: thesis: ex x being Element of [:(Fin A),(Fin A):] st S

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

thus S

A4: for b being Element of DISJOINT_PAIRS A st b in @ u holds

S

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

then reconsider d = FinPairUnion ((@ u),((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A))))) as Element of DISJOINT_PAIRS A by NORMFORM:21, NORMFORM:26;((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;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

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