let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for u being Element of ()
for K being Element of Normal_forms_on A st a in K ^ (K =>> (@ u)) holds
ex b being Element of DISJOINT_PAIRS A st
( b in u & b c= a )

let a be Element of DISJOINT_PAIRS A; :: thesis: for u being Element of ()
for K being Element of Normal_forms_on A st a in K ^ (K =>> (@ u)) holds
ex b being Element of DISJOINT_PAIRS A st
( b in u & b c= a )

let u be Element of (); :: thesis: for K being Element of Normal_forms_on A st a in K ^ (K =>> (@ u)) holds
ex b being Element of DISJOINT_PAIRS A st
( b in u & b c= a )

let K be Element of Normal_forms_on A; :: thesis: ( a in K ^ (K =>> (@ u)) implies ex b being Element of DISJOINT_PAIRS A st
( b in u & b c= a ) )

assume a in K ^ (K =>> (@ u)) ; :: thesis: ex b being Element of DISJOINT_PAIRS A st
( b in u & b c= a )

then consider b, c being Element of DISJOINT_PAIRS A such that
A1: b in K and
A2: c in K =>> (@ u) and
A3: a = b \/ c by NORMFORM:34;
consider f being Element of Funcs ((),[:(Fin A),(Fin A):]) such that
A4: f .: K c= u and
A5: c = FinPairUnion (K,(() .: (f,()))) by ;
A6: f . b in f .: K by ;
u = @ u ;
then reconsider d = f . b as Element of DISJOINT_PAIRS A by ;
take d ; :: thesis: ( d in u & d c= a )
thus d in u by A4, A6; :: thesis: d c= a
((pair_diff A) .: (f,())) . b = (f . b) \ b by Lm5;
hence d c= a by ; :: thesis: verum