let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A

for u being Element of (NormForm A)

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 (NormForm A)

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 (NormForm A); :: 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 ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) such that

A4: f .: K c= u and

A5: c = FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) by A2, Th18;

A6: f . b in f .: K by A1, FUNCT_2:35;

u = @ u ;

then reconsider d = f . b as Element of DISJOINT_PAIRS A by A4, A6, SETWISEO:9;

take d ; :: thesis: ( d in u & d c= a )

thus d in u by A4, A6; :: thesis: d c= a

((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b by Lm5;

hence d c= a by A1, A3, A5, NORMFORM:14, NORMFORM:16; :: thesis: verum

for u being Element of (NormForm A)

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 (NormForm A)

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 (NormForm A); :: 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 ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) such that

A4: f .: K c= u and

A5: c = FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) by A2, Th18;

A6: f . b in f .: K by A1, FUNCT_2:35;

u = @ u ;

then reconsider d = f . b as Element of DISJOINT_PAIRS A by A4, A6, SETWISEO:9;

take d ; :: thesis: ( d in u & d c= a )

thus d in u by A4, A6; :: thesis: d c= a

((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) . b = (f . b) \ b by Lm5;

hence d c= a by A1, A3, A5, NORMFORM:14, NORMFORM:16; :: thesis: verum