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:55;
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, Th23;
A6: f . b in f .: K by A1, FUNCT_2:43;
u = @ u ;
then reconsider d = f . b as Element of DISJOINT_PAIRS A by A4, A6, SETWISEO:14;
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:30, NORMFORM:35; :: thesis: verum