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