let A be set ; 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; 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); ( ( 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 )
; ex b being Element of DISJOINT_PAIRS A st
( b in (@ u) =>> (@ v) & b c= a )
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
S1[b,f9 . b]
from FRAENKEL:sch 27(A2);
set d = FinPairUnion ((@ u),((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS 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;
take
d
; ( 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; d c= a
thus
d c= a
by A5, NORMFORM:21; verum