let A be set ; 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; 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); 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; ( 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))
; 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
; ( d in u & d c= a )
thus
d in u
by A4, A6; 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; verum