let A be set ; for a being Element of DISJOINT_PAIRS A
for K being Element of Normal_forms_on A st K ^ {a} = {} holds
ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )
let a be Element of DISJOINT_PAIRS A; for K being Element of Normal_forms_on A st K ^ {a} = {} holds
ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )
let K be Element of Normal_forms_on A; ( K ^ {a} = {} implies ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a ) )
assume A1:
K ^ {a} = {}
; ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )
now ex c being Element of DISJOINT_PAIRS A st
( c in - K & c c= a )per cases
( not A is empty or A is empty )
;
suppose A14:
A is
empty
;
ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )reconsider Z =
{[{},{}]} as
Element of
Normal_forms_on {} by Th17;
take b =
a;
( b in - K & b c= a )A15:
a = [{},{}]
by A14, Th15;
mi (Z ^ Z) <> {}
by Th3;
then
K <> {[{},{}]}
by A1, A14, A15, NORMFORM:40, XBOOLE_1:3;
then
K = {}
by A14, Lm4, TARSKI:def 2;
then
- K = {[{},{}]}
by Th13;
hence
b in - K
by A15, TARSKI:def 1;
b c= athus
b c= a
;
verum end; end; end;
hence
ex b being Element of DISJOINT_PAIRS A st
( b in - K & b c= a )
; verum