:: HEYTING1 semantic presentation

{} is empty V7() non-empty empty-yielding finite finite-yielding V27() set
the empty V7() non-empty empty-yielding finite finite-yielding V27() set is empty V7() non-empty empty-yielding finite finite-yielding V27() set
1 is non empty set
{{},1} is non empty finite set
K162() is set
bool K162() is non empty cup-closed diff-closed preBoolean set
Fin {} is non empty cup-closed diff-closed preBoolean set
{{}} is non empty finite V27() set
bool {} is non empty finite V27() cup-closed diff-closed preBoolean set
A is non empty set
O is non empty set
[:A,O:] is non empty V7() set
bool [:A,O:] is non empty cup-closed diff-closed preBoolean set
sd is non empty set
[:A,sd:] is non empty V7() set
bool [:A,sd:] is non empty cup-closed diff-closed preBoolean set
F is non empty V7() V10(A) V11(O) Function-like V17(A) quasi_total Element of bool [:A,O:]
dom F is non empty Element of bool A
bool A is non empty cup-closed diff-closed preBoolean set
w is set
F . w is set
A is non empty set
Fin A is non empty cup-closed diff-closed preBoolean set
O is finite Element of Fin A
sd is finite Element of Fin A
F is Element of A
F is set
A is set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
O is finite Element of Fin (DISJOINT_PAIRS A)
mi O is Element of Normal_forms_on A
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in O or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in O & b₂ c= b₁ ) ) ) } is set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
O is Element of DISJOINT_PAIRS A
{.O.} is non empty finite Element of Fin (DISJOINT_PAIRS A)
F is Element of DISJOINT_PAIRS A
sd is finite Element of Fin (DISJOINT_PAIRS A)
w is Element of DISJOINT_PAIRS A
{O} is non empty V7() V10( Fin A) V11( Fin A) finite Element of bool (DISJOINT_PAIRS A)
bool (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
the Element of DISJOINT_PAIRS A is Element of DISJOINT_PAIRS A
{ the Element of DISJOINT_PAIRS A} is non empty V7() V10( Fin A) V11( Fin A) finite Element of bool (DISJOINT_PAIRS A)
bool (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
O is Element of DISJOINT_PAIRS A
{O} is non empty finite set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
O is Element of the carrier of (NormForm A)
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
O is Element of Normal_forms_on A
O ^ O is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in O & b₂ in O ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in O & b₂ in O ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (O ^ O) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in O ^ O or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in O ^ O & b₂ c= b₁ ) ) ) } is set
mi O is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in O or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in O & b₂ c= b₁ ) ) ) } is set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
O is Element of Normal_forms_on A
sd is set
F is finite Element of Fin (DISJOINT_PAIRS A)
w is Element of DISJOINT_PAIRS A
pf is Element of DISJOINT_PAIRS A
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
O is Element of the carrier of (NormForm A)
sd is set
(A,O) is Element of Normal_forms_on A
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
singleton (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):]
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
[:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set
bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set
dom (singleton (DISJOINT_PAIRS A)) is non empty V7() V10( Fin A) V11( Fin A) Element of bool (DISJOINT_PAIRS A)
bool (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
sd is set
F is Element of DISJOINT_PAIRS A
(singleton (DISJOINT_PAIRS A)) . F is finite Element of Fin (DISJOINT_PAIRS A)
(A,F) is non empty finite Element of Normal_forms_on A
(singleton (DISJOINT_PAIRS A)) . sd is set
sd is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
F is Element of DISJOINT_PAIRS A
sd . F is Element of the carrier of (NormForm A)
(A,F) is non empty finite Element of Normal_forms_on A
O is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
sd is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
F is Element of DISJOINT_PAIRS A
O . F is Element of the carrier of (NormForm A)
(A,F) is non empty finite Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
sd . F is Element of the carrier of (NormForm A)
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
O is Element of DISJOINT_PAIRS A
sd is Element of DISJOINT_PAIRS A
(A) . sd is Element of the carrier of (NormForm A)
(A,sd) is non empty finite Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
O is Element of DISJOINT_PAIRS A
(A) . O is Element of the carrier of (NormForm A)
(A,O) is non empty finite Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
singleton (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):]
[:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set
bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set
O is Element of DISJOINT_PAIRS A
(A) . O is Element of the carrier of (NormForm A)
(singleton (DISJOINT_PAIRS A)) . O is finite Element of Fin (DISJOINT_PAIRS A)
(A,O) is non empty finite Element of Normal_forms_on A
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
the carrier of (NormForm A) is non empty set
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
singleton (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):]
[:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set
bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set
O is Element of Normal_forms_on A
FinJoin (O,(A)) is Element of the carrier of (NormForm A)
FinUnion (O,(singleton (DISJOINT_PAIRS A))) is finite Element of Fin (DISJOINT_PAIRS A)
mi (FinUnion (O,(singleton (DISJOINT_PAIRS A)))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in FinUnion (O,(singleton (DISJOINT_PAIRS A))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in FinUnion (O,(singleton (DISJOINT_PAIRS A))) & b₂ c= b₁ ) ) ) } is set
sd is Element of DISJOINT_PAIRS A
F is Element of DISJOINT_PAIRS A
(singleton (DISJOINT_PAIRS A)) . F is finite Element of Fin (DISJOINT_PAIRS A)
w is Element of DISJOINT_PAIRS A
pf is Element of DISJOINT_PAIRS A
(singleton (DISJOINT_PAIRS A)) . pf is finite Element of Fin (DISJOINT_PAIRS A)
[:(Fin (DISJOINT_PAIRS A)),(Normal_forms_on A):] is non empty V7() set
bool [:(Fin (DISJOINT_PAIRS A)),(Normal_forms_on A):] is non empty cup-closed diff-closed preBoolean set
sd is non empty V7() V10( Fin (DISJOINT_PAIRS A)) V11( Normal_forms_on A) Function-like V17( Fin (DISJOINT_PAIRS A)) quasi_total Element of bool [:(Fin (DISJOINT_PAIRS A)),(Normal_forms_on A):]
[:(Fin (DISJOINT_PAIRS A)), the carrier of (NormForm A):] is non empty V7() set
bool [:(Fin (DISJOINT_PAIRS A)), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
F is non empty V7() V10( Fin (DISJOINT_PAIRS A)) V11( the carrier of (NormForm A)) Function-like V17( Fin (DISJOINT_PAIRS A)) quasi_total Element of bool [:(Fin (DISJOINT_PAIRS A)), the carrier of (NormForm A):]
{}. (DISJOINT_PAIRS A) is empty V7() non-empty empty-yielding finite finite-yielding V27() Element of Fin (DISJOINT_PAIRS A)
F . ({}. (DISJOINT_PAIRS A)) is Element of the carrier of (NormForm A)
mi ({}. (DISJOINT_PAIRS A)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in {}. (DISJOINT_PAIRS A) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in {}. (DISJOINT_PAIRS A) & b₂ c= b₁ ) ) ) } is set
Bottom (NormForm A) is Element of the carrier of (NormForm A)
the L_join of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
the_unity_wrt the L_join of (NormForm A) is Element of the carrier of (NormForm A)
w is finite Element of Fin (DISJOINT_PAIRS A)
F . w is Element of the carrier of (NormForm A)
(A,(F . w)) is Element of Normal_forms_on A
mi w is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in w or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in w & b₂ c= b₁ ) ) ) } is set
pf is finite Element of Fin (DISJOINT_PAIRS A)
F . pf is Element of the carrier of (NormForm A)
(A,(F . pf)) is Element of Normal_forms_on A
mi pf is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in pf or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in pf & b₂ c= b₁ ) ) ) } is set
w \/ pf is finite Element of Fin (DISJOINT_PAIRS A)
F . (w \/ pf) is Element of the carrier of (NormForm A)
mi (w \/ pf) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in w \/ pf or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in w \/ pf & b₂ c= b₁ ) ) ) } is set
(mi w) \/ pf is finite Element of Fin (DISJOINT_PAIRS A)
mi ((mi w) \/ pf) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (mi w) \/ pf or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (mi w) \/ pf & b₂ c= b₁ ) ) ) } is set
(mi w) \/ (mi pf) is finite Element of Fin (DISJOINT_PAIRS A)
mi ((mi w) \/ (mi pf)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (mi w) \/ (mi pf) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (mi w) \/ (mi pf) & b₂ c= b₁ ) ) ) } is set
the L_join of (NormForm A) . ((F . w),(F . pf)) is Element of the carrier of (NormForm A)
F * (singleton (DISJOINT_PAIRS A)) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
w is Element of DISJOINT_PAIRS A
(F * (singleton (DISJOINT_PAIRS A))) . w is Element of the carrier of (NormForm A)
(singleton (DISJOINT_PAIRS A)) . w is finite Element of Fin (DISJOINT_PAIRS A)
F . ((singleton (DISJOINT_PAIRS A)) . w) is Element of the carrier of (NormForm A)
(A,w) is non empty finite Element of Normal_forms_on A
F . (A,w) is Element of the carrier of (NormForm A)
mi (A,w) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,w) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,w) & b₂ c= b₁ ) ) ) } is set
(A) . w is Element of the carrier of (NormForm A)
the L_join of (NormForm A) $$ (O,(A)) is Element of the carrier of (NormForm A)
the L_join of (NormForm A) $$ (O,(F * (singleton (DISJOINT_PAIRS A)))) is Element of the carrier of (NormForm A)
F . (FinUnion (O,(singleton (DISJOINT_PAIRS A)))) is Element of the carrier of (NormForm A)
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
O is Element of the carrier of (NormForm A)
(A,O) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
FinJoin ((A,O),(A)) is Element of the carrier of (NormForm A)
singleton (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):]
[:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set
bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set
FinUnion ((A,O),(singleton (DISJOINT_PAIRS A))) is finite Element of Fin (DISJOINT_PAIRS A)
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
O is Element of the carrier of (NormForm A)
sd is Element of the carrier of (NormForm A)
O "\/" sd is Element of the carrier of (NormForm A)
the L_join of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (NormForm A) . (O,sd) is Element of the carrier of (NormForm A)
(A,O) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A,sd) is Element of Normal_forms_on A
(A,O) \/ (A,sd) is finite Element of Fin (DISJOINT_PAIRS A)
mi ((A,O) \/ (A,sd)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,O) \/ (A,sd) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,O) \/ (A,sd) & b₂ c= b₁ ) ) ) } is set
F is Element of [:(Fin A),(Fin A):]
w is Element of DISJOINT_PAIRS A
O \/ sd is set
pf is Element of DISJOINT_PAIRS A
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
O is Element of the carrier of (NormForm A)
sd is Element of the carrier of (NormForm A)
(A,O) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A,sd) is Element of Normal_forms_on A
(A,O) \/ (A,sd) is finite Element of Fin (DISJOINT_PAIRS A)
mi ((A,O) \/ (A,sd)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,O) \/ (A,sd) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,O) \/ (A,sd) & b₂ c= b₁ ) ) ) } is set
F is Element of DISJOINT_PAIRS A
O \/ sd is set
w is Element of DISJOINT_PAIRS A
F is Element of DISJOINT_PAIRS A
mi (A,sd) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,sd) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,sd) & b₂ c= b₁ ) ) ) } is set
w is Element of DISJOINT_PAIRS A
O \/ sd is set
pf is Element of DISJOINT_PAIRS A
O "\/" sd is Element of the carrier of (NormForm A)
the L_join of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
the L_join of (NormForm A) . (O,sd) is Element of the carrier of (NormForm A)
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
O is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
sd is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
F is Element of [:(Fin A),(Fin A):]
w is Element of [:(Fin A),(Fin A):]
O . (F,w) is Element of [:(Fin A),(Fin A):]
F \ w is Element of [:(Fin A),(Fin A):]
F `1 is finite Element of Fin A
w `1 is finite Element of Fin A
(F `1) \ (w `1) is finite Element of Fin A
F `2 is finite Element of Fin A
w `2 is finite Element of Fin A
(F `2) \ (w `2) is finite Element of Fin A
[((F `1) \ (w `1)),((F `2) \ (w `2))] is V1() Element of [:(Fin A),(Fin A):]
{((F `1) \ (w `1)),((F `2) \ (w `2))} is non empty finite V27() set
{((F `1) \ (w `1))} is non empty finite V27() set
{{((F `1) \ (w `1)),((F `2) \ (w `2))},{((F `1) \ (w `1))}} is non empty finite V27() set
sd . (F,w) is Element of [:(Fin A),(Fin A):]
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
O is finite Element of Fin (DISJOINT_PAIRS A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in O ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in O ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in O ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in O ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
{ ((b₁ `1) \/ (b<sub>1</sub> `2)) where b₁ is Element of DISJOINT_PAIRS A : b₁ in O } is set
union { ((b₁ `1) \/ (b<sub>1</sub> `2)) where b₁ is Element of DISJOINT_PAIRS A : b₁ in O } is set
{ (a₁ . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( a₁ . b₁ in b₁ `2 & b<sub>1</sub> in O ) } is set
{ (a<sub>1</sub> . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( a<sub>1</sub> . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } is set
[ { (a₁ . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( a₁ . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (a<sub>1</sub> . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( a<sub>1</sub> . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } ] is V1() set
{ { (a₁ . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( a₁ . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (a<sub>1</sub> . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( a<sub>1</sub> . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } } is non empty finite set
{ { (a₁ . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( a₁ . b₁ in b₁ `2 & b<sub>1</sub> in O ) } } is non empty finite set
{{ { (a<sub>1</sub> . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( a<sub>1</sub> . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } , { (a₁ . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( a₁ . b₁ in b₁ `1 & b<sub>1</sub> in O ) } },{ { (a<sub>1</sub> . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( a<sub>1</sub> . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } }} is non empty finite V27() set
{ H₂(b₁) where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
{ H₂(b₁) where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : b₁ .: O c= union { ((b₁ `1) \/ (b<sub>1</sub> `2)) where b₂ is Element of DISJOINT_PAIRS A : b₁ in O } } is set
(DISJOINT_PAIRS A) /\ { H₂(b₁) where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
pf is set
sf is Element of DISJOINT_PAIRS A
sf `1 is finite Element of Fin A
sf `2 is finite Element of Fin A
(sf `1) \/ (sf `2) is finite Element of Fin A
pf is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))
sf is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))
pf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11((A)) Function-like finite Element of bool [:(DISJOINT_PAIRS A),(A):]
[:(DISJOINT_PAIRS A),(A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A),(A):] is non empty cup-closed diff-closed preBoolean set
sf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11((A)) Function-like finite Element of bool [:(DISJOINT_PAIRS A),(A):]
a is Element of DISJOINT_PAIRS A
pf . a is set
a `1 is set
sf . a is set
{ (pf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( S<sub>3</sub>[b<sub>1</sub>] & b<sub>1</sub> in O ) } is set
{ (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( S<sub>5</sub>[b<sub>1</sub>] & b<sub>1</sub> in O ) } is set
a is Element of DISJOINT_PAIRS A
pf . a is set
a `2 is set
sf . a is set
{ (pf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( S₄[b₁] & b₁ in O ) } is set
{ (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( S₆[b₁] & b₁ in O ) } is set
{ (pf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( pf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } is set
{ (pf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( pf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } is set
[ { (pf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( pf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (pf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( pf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } ] is V1() set
{ { (pf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( pf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (pf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( pf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } } is non empty finite set
{ { (pf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( pf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } } is non empty finite set
{{ { (pf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( pf . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } , { (pf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( pf . b₁ in b₁ `1 & b<sub>1</sub> in O ) } },{ { (pf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( pf . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } }} is non empty finite V27() set
{ (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } is set
{ (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } is set
[ { (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } ] is V1() set
{ { (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } } is non empty finite set
{ { (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } } is non empty finite set
{{ { (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } , { (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `1 & b<sub>1</sub> in O ) } },{ { (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } }} is non empty finite V27() set
pf is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))
pf .: O is finite set
sf is set
pf .: O is finite Element of Fin (A)
Fin (A) is non empty cup-closed diff-closed preBoolean set
dom pf is V7() V10( Fin A) V11( Fin A) Element of bool (DISJOINT_PAIRS A)
bool (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
a is set
pf . a is set
v is Element of DISJOINT_PAIRS A
v `1 is finite Element of Fin A
v `2 is finite Element of Fin A
(v `1) \/ (v `2) is finite Element of Fin A
pf . v is Element of (A)
{ H₂(b₁) where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : S₂[b₁] } is set
{ H₂(b₁) where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Element of DISJOINT_PAIRS A : b₁ in O } is set
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
sd is finite Element of Fin (DISJOINT_PAIRS A)
{ (FinPairUnion (O,((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: O c= sd } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion (O,((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: O c= sd } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
pf is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
pf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like finite Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
sf is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
sf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like finite Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
(A) .: (pf,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
((A) .: (pf,(incl (DISJOINT_PAIRS A)))) | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like finite Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
(A) .: (sf,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
((A) .: (sf,(incl (DISJOINT_PAIRS A)))) | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like finite Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
FinPairUnion (O,((A) .: (pf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
FinPairUnion A is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total commutative associative idempotent Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
(FinPairUnion A) $$ (O,((A) .: (pf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
FinPairUnion (O,((A) .: (sf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
(FinPairUnion A) $$ (O,((A) .: (sf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
{ H₁(b₁) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: O c= sd } is set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
O is finite Element of Fin (DISJOINT_PAIRS A)
(A,O) is finite Element of Fin (DISJOINT_PAIRS A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in O ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in O ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in O ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in O ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
sd is Element of DISJOINT_PAIRS A
F is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))
{ (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in O ) } is set
{ (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } is set
[ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } ] is V1() set
{ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } } is non empty finite set
{ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in O ) } } is non empty finite set
{{ { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } , { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `1 & b<sub>1</sub> in O ) } },{ { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } }} is non empty finite V27() set
[{},{}] is V1() set
{{},{}} is non empty finite V27() set
{{{},{}},{{}}} is non empty finite V27() set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
{}. A is empty V7() non-empty empty-yielding finite finite-yielding V27() Element of Fin A
[({}. A),({}. A)] is V1() Element of [:(Fin A),(Fin A):]
{({}. A),({}. A)} is non empty finite V27() set
{({}. A)} is non empty finite V27() set
{{({}. A),({}. A)},{({}. A)}} is non empty finite V27() set
[{},{}] `1 is set
[{},{}] `2 is set
{[{},{}]} is non empty V7() finite set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
O is Element of Normal_forms_on A
(A,O) is finite Element of Fin (DISJOINT_PAIRS A)
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in O ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in O ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in O ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in O ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
sd is set
F is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))
{ (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in O ) } is set
{ (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } is set
[ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } ] is V1() set
{ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } } is non empty finite set
{ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in O ) } } is non empty finite set
{{ { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } , { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `1 & b<sub>1</sub> in O ) } },{ { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } }} is non empty finite V27() set
sd `2 is set
the Element of sd `2 is Element of sd `2
pf is Element of DISJOINT_PAIRS A
F . pf is Element of (A)
pf `1 is finite Element of Fin A
sd `1 is set
the Element of sd `1 is Element of sd `1
pf is Element of DISJOINT_PAIRS A
F . pf is Element of (A)
pf `2 is finite Element of Fin A
the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))
F is set
{ ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b₁ in b₁ `2 & b<sub>1</sub> in O ) } is set
the Element of { ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } is Element of { ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b₁ in b₁ `2 & b<sub>1</sub> in O ) }
pf is Element of DISJOINT_PAIRS A
the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . pf is Element of (A)
pf `2 is finite Element of Fin A
{ ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b₁ in b₁ `1 & b<sub>1</sub> in O ) } is set
the Element of { ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } is Element of { ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b₁ in b₁ `1 & b<sub>1</sub> in O ) }
pf is Element of DISJOINT_PAIRS A
the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . pf is Element of (A)
pf `1 is finite Element of Fin A
w is Element of DISJOINT_PAIRS A
the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . w is Element of (A)
w `1 is finite Element of Fin A
w `2 is finite Element of Fin A
(w `1) \/ (w `2) is finite Element of Fin A
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
O is Element of Normal_forms_on A
sd is Element of Normal_forms_on A
(A,O,sd) is finite Element of Fin (DISJOINT_PAIRS A)
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion (O,((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: O c= sd } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion (O,((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: O c= sd } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
{}. A is empty V7() non-empty empty-yielding finite finite-yielding V27() Element of Fin A
{}. (DISJOINT_PAIRS A) is empty V7() non-empty empty-yielding finite finite-yielding V27() Element of Fin (DISJOINT_PAIRS A)
F is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
(A) .: (F,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
FinPairUnion (O,((A) .: (F,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
FinPairUnion A is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total commutative associative idempotent Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
(FinPairUnion A) $$ (O,((A) .: (F,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
the_unity_wrt (FinPairUnion A) is Element of [:(Fin A),(Fin A):]
F is set
w is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
(A) .: (w,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
FinPairUnion (O,((A) .: (w,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
(FinPairUnion A) $$ (O,((A) .: (w,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
w .: O is finite Element of Fin [:(Fin A),(Fin A):]
Fin [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
w is set
(A) .: ( the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
FinPairUnion (O,((A) .: ( the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
(FinPairUnion A) $$ (O,((A) .: ( the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) .: O is finite Element of Fin [:(Fin A),(Fin A):]
Fin [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
[:(Fin {}),(Fin {}):] is non empty V7() set
DISJOINT_PAIRS {} is non empty V7() V10( Fin {}) V11( Fin {}) Element of bool [:(Fin {}),(Fin {}):]
bool [:(Fin {}),(Fin {}):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin {}),(Fin {}):] : b₁ `1 misses b<sub>1</sub> `2 } is set
A is Element of DISJOINT_PAIRS {}
O is finite Element of Fin {}
sd is finite Element of Fin {}
[O,sd] is V1() Element of [:(Fin {}),(Fin {}):]
{O,sd} is non empty finite V27() set
{O} is non empty finite V27() set
{{O,sd},{O}} is non empty finite V27() set
A is set
A is set
Fin (DISJOINT_PAIRS {}) is non empty cup-closed diff-closed preBoolean set
{{},{[{},{}]}} is non empty finite V27() set
bool (DISJOINT_PAIRS {}) is non empty cup-closed diff-closed preBoolean set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
sd is Element of DISJOINT_PAIRS A
O is finite Element of Fin (DISJOINT_PAIRS A)
F is Element of DISJOINT_PAIRS A
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
O is finite Element of Fin (DISJOINT_PAIRS A)
sd is finite Element of Fin (DISJOINT_PAIRS A)
(A,O,sd) is finite Element of Fin (DISJOINT_PAIRS A)
{ (FinPairUnion (O,((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: O c= sd } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion (O,((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: O c= sd } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
F is Element of DISJOINT_PAIRS A
w is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
(A) .: (w,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
FinPairUnion (O,((A) .: (w,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
FinPairUnion A is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total commutative associative idempotent Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
(FinPairUnion A) $$ (O,((A) .: (w,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
w .: O is finite Element of Fin [:(Fin A),(Fin A):]
Fin [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
O is Element of DISJOINT_PAIRS A
(A,O) is non empty finite Element of Normal_forms_on A
sd is Element of Normal_forms_on A
sd ^ (A,O) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in sd & b₂ in (A,O) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in sd & b₂ in (A,O) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
(A,sd) is finite Element of Fin (DISJOINT_PAIRS A)
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in sd ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in sd ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in sd or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in sd ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in sd ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in sd or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
O `2 is finite Element of Fin A
O `1 is finite Element of Fin A
F is Element of DISJOINT_PAIRS A
F \/ O is Element of [:(Fin A),(Fin A):]
F `1 is finite Element of Fin A
(F `1) \/ (O `1) is finite Element of Fin A
F `2 is finite Element of Fin A
(F `2) \/ (O `2) is finite Element of Fin A
[((F `1) \/ (O `1)),((F `2) \/ (O `2))] is V1() Element of [:(Fin A),(Fin A):]
{((F `1) \/ (O `1)),((F `2) \/ (O `2))} is non empty finite V27() set
{((F `1) \/ (O `1))} is non empty finite V27() set
{{((F `1) \/ (O `1)),((F `2) \/ (O `2))},{((F `1) \/ (O `1))}} is non empty finite V27() set
w is Element of (A)
pf is Element of (A)
(F `1) /\ (O `2) is finite Element of Fin A
(F `2) /\ (O `1) is finite Element of Fin A
F `1 is set
(F `1) /\ (O `2) is finite set
F `2 is set
(F `2) /\ (O `1) is finite set
((F `1) /\ (O `2)) \/ ((F `2) /\ (O `1)) is finite set
F is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))
{ (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in sd ) } is set
{ (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in sd ) } is set
sf is set
a is Element of DISJOINT_PAIRS A
F . a is Element of (A)
a `1 is finite Element of Fin A
(a `1) /\ (O `2) is finite Element of Fin A
a `2 is finite Element of Fin A
(a `2) /\ (O `1) is finite Element of Fin A
((a `1) /\ (O `2)) \/ ((a `2) /\ (O `1)) is finite Element of Fin A
sf is set
a is Element of DISJOINT_PAIRS A
F . a is Element of (A)
a `2 is finite Element of Fin A
a `1 is finite Element of Fin A
(a `1) /\ (O `2) is finite Element of Fin A
(a `2) /\ (O `1) is finite Element of Fin A
((a `1) /\ (O `2)) \/ ((a `2) /\ (O `1)) is finite Element of Fin A
[ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in sd ) } , { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in sd ) } ] is V1() set
{ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in sd ) } , { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in sd ) } } is non empty finite set
{ { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `2 & b<sub>1</sub> in sd ) } } is non empty finite set
{{ { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in sd ) } , { (F . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( F . b₁ in b₁ `1 & b<sub>1</sub> in sd ) } },{ { (F . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( F . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in sd ) } }} is non empty finite V27() set
sf is Element of DISJOINT_PAIRS A
v is Element of DISJOINT_PAIRS A
F . v is Element of (A)
v `1 is finite Element of Fin A
(v `1) /\ (O `2) is finite Element of Fin A
v `2 is finite Element of Fin A
(v `2) /\ (O `1) is finite Element of Fin A
((v `1) /\ (O `2)) \/ ((v `2) /\ (O `1)) is finite Element of Fin A
(v `1) \/ (v `2) is finite Element of Fin A
a is Element of DISJOINT_PAIRS A
a `1 is finite Element of Fin A
a `2 is finite Element of Fin A
Normal_forms_on {} is non empty Element of bool (Fin (DISJOINT_PAIRS {}))
bool (Fin (DISJOINT_PAIRS {})) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS {}) : for b₂, b₃ being Element of DISJOINT_PAIRS {} holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
F is Element of Normal_forms_on {}
F ^ F is finite Element of Fin (DISJOINT_PAIRS {})
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS {} : ( b₁ in F & b₂ in F ) } is set
(DISJOINT_PAIRS {}) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS {} : ( b₁ in F & b₂ in F ) } is V7() V10( Fin {}) V11( Fin {}) Element of bool [:(Fin {}),(Fin {}):]
mi (F ^ F) is Element of Normal_forms_on {}
{ b₁ where b₁ is Element of DISJOINT_PAIRS {} : for b₂ being Element of DISJOINT_PAIRS {} holds
( ( not b₂ in F ^ F or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in F ^ F & b₂ c= b₁ ) ) ) } is set
w is Element of DISJOINT_PAIRS A
F is Element of DISJOINT_PAIRS A
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
F is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
(A) .: (F,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
sd is Element of DISJOINT_PAIRS A
((A) .: (F,(incl (DISJOINT_PAIRS A)))) . sd is Element of [:(Fin A),(Fin A):]
F . sd is Element of [:(Fin A),(Fin A):]
(incl (DISJOINT_PAIRS A)) . sd is Element of [:(Fin A),(Fin A):]
(A) . ((F . sd),((incl (DISJOINT_PAIRS A)) . sd)) is Element of [:(Fin A),(Fin A):]
(A) . ((F . sd),sd) is Element of [:(Fin A),(Fin A):]
(F . sd) \ sd is Element of [:(Fin A),(Fin A):]
(F . sd) `1 is finite Element of Fin A
sd `1 is finite Element of Fin A
((F . sd) `1) \ (sd `1) is finite Element of Fin A
(F . sd) `2 is finite Element of Fin A
sd `2 is finite Element of Fin A
((F . sd) `2) \ (sd `2) is finite Element of Fin A
[(((F . sd) `1) \ (sd `1)),(((F . sd) `2) \ (sd `2))] is V1() Element of [:(Fin A),(Fin A):]
{(((F . sd) `1) \ (sd `1)),(((F . sd) `2) \ (sd `2))} is non empty finite V27() set
{(((F . sd) `1) \ (sd `1))} is non empty finite V27() set
{{(((F . sd) `1) \ (sd `1)),(((F . sd) `2) \ (sd `2))},{(((F . sd) `1) \ (sd `1))}} is non empty finite V27() set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
O is Element of DISJOINT_PAIRS A
sd is Element of the carrier of (NormForm A)
(A,sd) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
F is Element of the carrier of (NormForm A)
(A,F) is Element of Normal_forms_on A
(A,(A,sd),(A,F)) is finite Element of Fin (DISJOINT_PAIRS A)
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) V11( DISJOINT_PAIRS A) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion ((A,sd),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,sd) c= (A,F) } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion ((A,sd),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,sd) c= (A,F) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
w is Element of DISJOINT_PAIRS A
w \/ O is Element of [:(Fin A),(Fin A):]
w `1 is finite Element of Fin A
O `1 is finite Element of Fin A
(w `1) \/ (O `1) is finite Element of Fin A
w `2 is finite Element of Fin A
O `2 is finite Element of Fin A
(w `2) \/ (O `2) is finite Element of Fin A
[((w `1) \/ (O `1)),((w `2) \/ (O `2))] is V1() Element of [:(Fin A),(Fin A):]
{((w `1) \/ (O `1)),((w `2) \/ (O `2))} is non empty finite V27() set
{((w `1) \/ (O `1))} is non empty finite V27() set
{{((w `1) \/ (O `1)),((w `2) \/ (O `2))},{((w `1) \/ (O `1))}} is non empty finite V27() set
pf is Element of DISJOINT_PAIRS A
sf is Element of [:(Fin A),(Fin A):]
a is Element of [:(Fin A),(Fin A):]
w is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
(A) .: (w,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
FinPairUnion ((A,sd),((A) .: (w,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
FinPairUnion A is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total commutative associative idempotent Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
(FinPairUnion A) $$ ((A,sd),((A) .: (w,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
sf is Element of DISJOINT_PAIRS A
w . sf is Element of [:(Fin A),(Fin A):]
O \/ sf is Element of [:(Fin A),(Fin A):]
sf `1 is finite Element of Fin A
(O `1) \/ (sf `1) is finite Element of Fin A
sf `2 is finite Element of Fin A
(O `2) \/ (sf `2) is finite Element of Fin A
[((O `1) \/ (sf `1)),((O `2) \/ (sf `2))] is V1() Element of [:(Fin A),(Fin A):]
{((O `1) \/ (sf `1)),((O `2) \/ (sf `2))} is non empty finite V27() set
{((O `1) \/ (sf `1))} is non empty finite V27() set
{{((O `1) \/ (sf `1)),((O `2) \/ (sf `2))},{((O `1) \/ (sf `1))}} is non empty finite V27() set
((A) .: (w,(incl (DISJOINT_PAIRS A)))) . sf is Element of [:(Fin A),(Fin A):]
(w . sf) \ sf is Element of [:(Fin A),(Fin A):]
(w . sf) `1 is finite Element of Fin A
((w . sf) `1) \ (sf `1) is finite Element of Fin A
(w . sf) `2 is finite Element of Fin A
((w . sf) `2) \ (sf `2) is finite Element of Fin A
[(((w . sf) `1) \ (sf `1)),(((w . sf) `2) \ (sf `2))] is V1() Element of [:(Fin A),(Fin A):]
{(((w . sf) `1) \ (sf `1)),(((w . sf) `2) \ (sf `2))} is non empty finite V27() set
{(((w . sf) `1) \ (sf `1))} is non empty finite V27() set
{{(((w . sf) `1) \ (sf `1)),(((w . sf) `2) \ (sf `2))},{(((w . sf) `1) \ (sf `1))}} is non empty finite V27() set
sf is Element of DISJOINT_PAIRS A
a is Element of DISJOINT_PAIRS A
w . a is Element of [:(Fin A),(Fin A):]
w .: (A,sd) is finite Element of Fin [:(Fin A),(Fin A):]
Fin [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion ((A,sd),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,sd) c= F } is set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
O is Element of DISJOINT_PAIRS A
sd is Element of the carrier of (NormForm A)
(A,sd) is Element of Normal_forms_on A
F is Element of Normal_forms_on A
(A,F,(A,sd)) is finite Element of Fin (DISJOINT_PAIRS A)
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) V11( DISJOINT_PAIRS A) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion (F,((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: F c= (A,sd) } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion (F,((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: F c= (A,sd) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
F ^ (A,F,(A,sd)) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in F & b₂ in (A,F,(A,sd)) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in F & b₂ in (A,F,(A,sd)) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
w is Element of DISJOINT_PAIRS A
pf is Element of DISJOINT_PAIRS A
w \/ pf is Element of [:(Fin A),(Fin A):]
w `1 is finite Element of Fin A
pf `1 is finite Element of Fin A
(w `1) \/ (pf `1) is finite Element of Fin A
w `2 is finite Element of Fin A
pf `2 is finite Element of Fin A
(w `2) \/ (pf `2) is finite Element of Fin A
[((w `1) \/ (pf `1)),((w `2) \/ (pf `2))] is V1() Element of [:(Fin A),(Fin A):]
{((w `1) \/ (pf `1)),((w `2) \/ (pf `2))} is non empty finite V27() set
{((w `1) \/ (pf `1))} is non empty finite V27() set
{{((w `1) \/ (pf `1)),((w `2) \/ (pf `2))},{((w `1) \/ (pf `1))}} is non empty finite V27() set
sf is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])
sf .: F is finite Element of Fin [:(Fin A),(Fin A):]
Fin [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
(A) .: (sf,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
FinPairUnion (F,((A) .: (sf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
FinPairUnion A is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total commutative associative idempotent Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
(FinPairUnion A) $$ (F,((A) .: (sf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]
sf . w is Element of [:(Fin A),(Fin A):]
a is Element of DISJOINT_PAIRS A
((A) .: (sf,(incl (DISJOINT_PAIRS A)))) . w is Element of [:(Fin A),(Fin A):]
(sf . w) \ w is Element of [:(Fin A),(Fin A):]
(sf . w) `1 is finite Element of Fin A
((sf . w) `1) \ (w `1) is finite Element of Fin A
(sf . w) `2 is finite Element of Fin A
((sf . w) `2) \ (w `2) is finite Element of Fin A
[(((sf . w) `1) \ (w `1)),(((sf . w) `2) \ (w `2))] is V1() Element of [:(Fin A),(Fin A):]
{(((sf . w) `1) \ (w `1)),(((sf . w) `2) \ (w `2))} is non empty finite V27() set
{(((sf . w) `1) \ (w `1))} is non empty finite V27() set
{{(((sf . w) `1) \ (w `1)),(((sf . w) `2) \ (w `2))},{(((sf . w) `1) \ (w `1))}} is non empty finite V27() set
A is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
O is Element of Normal_forms_on A
(A,O) is finite Element of Fin (DISJOINT_PAIRS A)
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in O ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in O ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in O ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in O ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in O or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
O ^ (A,O) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in O & b₂ in (A,O) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in O & b₂ in (A,O) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
the Element of O ^ (A,O) is Element of O ^ (A,O)
F is Element of DISJOINT_PAIRS A
w is Element of DISJOINT_PAIRS A
pf is Element of DISJOINT_PAIRS A
w \/ pf is Element of [:(Fin A),(Fin A):]
w `1 is finite Element of Fin A
pf `1 is finite Element of Fin A
(w `1) \/ (pf `1) is finite Element of Fin A
w `2 is finite Element of Fin A
pf `2 is finite Element of Fin A
(w `2) \/ (pf `2) is finite Element of Fin A
[((w `1) \/ (pf `1)),((w `2) \/ (pf `2))] is V1() Element of [:(Fin A),(Fin A):]
{((w `1) \/ (pf `1)),((w `2) \/ (pf `2))} is non empty finite V27() set
{((w `1) \/ (pf `1))} is non empty finite V27() set
{{((w `1) \/ (pf `1)),((w `2) \/ (pf `2))},{((w `1) \/ (pf `1))}} is non empty finite V27() set
F `1 is finite Element of Fin A
(w `1) \/ (pf `1) is finite Element of Fin A
F `2 is finite Element of Fin A
(w `2) \/ (pf `2) is finite Element of Fin A
sf is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))
{ (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } is set
{ (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } is set
[ { (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } ] is V1() set
{ { (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } , { (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `1 & b₁ in O ) } } is non empty finite set
{ { (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `2 & b<sub>1</sub> in O ) } } is non empty finite set
{{ { (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } , { (sf . b₁) where b₁ is Element of DISJOINT_PAIRS A : ( sf . b₁ in b₁ `1 & b<sub>1</sub> in O ) } },{ { (sf . b<sub>1</sub>) where b<sub>1</sub> is Element of DISJOINT_PAIRS A : ( sf . b<sub>1</sub> in b<sub>1</sub> `2 & b₁ in O ) } }} is non empty finite V27() set
sf . w is Element of (A)
(w `1) \/ (w `2) is finite Element of Fin A
(F `1) /\ (F `2) is finite Element of Fin A
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
[: the carrier of (NormForm A),(Normal_forms_on A):] is non empty V7() set
bool [: the carrier of (NormForm A),(Normal_forms_on A):] is non empty cup-closed diff-closed preBoolean set
O is non empty V7() V10( the carrier of (NormForm A)) V11( Normal_forms_on A) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A),(Normal_forms_on A):]
sd is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
F is Element of the carrier of (NormForm A)
sd . F is Element of the carrier of (NormForm A)
(A,F) is Element of Normal_forms_on A
(A,(A,F)) is finite Element of Fin (DISJOINT_PAIRS A)
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,F) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,F) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,F) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,F) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,F) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,F) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (A,(A,F)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,F)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,F)) & b₂ c= b₁ ) ) ) } is set
O is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
sd is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
F is Element of the carrier of (NormForm A)
O . F is Element of the carrier of (NormForm A)
(A,F) is Element of Normal_forms_on A
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A,(A,F)) is finite Element of Fin (DISJOINT_PAIRS A)
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,F) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,F) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,F) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,F) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,F) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,F) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (A,(A,F)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,F)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,F)) & b₂ c= b₁ ) ) ) } is set
sd . F is Element of the carrier of (NormForm A)
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):],(Normal_forms_on A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):],(Normal_forms_on A):] is non empty cup-closed diff-closed preBoolean set
O is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( Normal_forms_on A) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):],(Normal_forms_on A):]
sd is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
F is Element of the carrier of (NormForm A)
(A,F) is Element of Normal_forms_on A
w is Element of the carrier of (NormForm A)
sd . (F,w) is Element of the carrier of (NormForm A)
(A,w) is Element of Normal_forms_on A
(A,(A,F),(A,w)) is finite Element of Fin (DISJOINT_PAIRS A)
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion ((A,F),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,F) c= (A,w) } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion ((A,F),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,F) c= (A,w) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (A,(A,F),(A,w)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,F),(A,w)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,F),(A,w)) & b₂ c= b₁ ) ) ) } is set
O is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
sd is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
F is Element of the carrier of (NormForm A)
w is Element of the carrier of (NormForm A)
O . (F,w) is Element of the carrier of (NormForm A)
(A,F) is Element of Normal_forms_on A
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A,w) is Element of Normal_forms_on A
(A,(A,F),(A,w)) is finite Element of Fin (DISJOINT_PAIRS A)
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion ((A,F),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,F) c= (A,w) } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion ((A,F),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,F) c= (A,w) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (A,(A,F),(A,w)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,F),(A,w)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,F),(A,w)) & b₂ c= b₁ ) ) ) } is set
sd . (F,w) is Element of the carrier of (NormForm A)
O is Element of the carrier of (NormForm A)
bool O is non empty cup-closed diff-closed preBoolean set
Fin the carrier of (NormForm A) is non empty cup-closed diff-closed preBoolean set
sd is set
(A,O) is Element of Normal_forms_on A
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
(A,O) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
[: the carrier of (NormForm A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set
bool [: the carrier of (NormForm A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set
sd is non empty V7() V10( the carrier of (NormForm A)) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A),(Fin (DISJOINT_PAIRS A)):]
F is Element of the carrier of (NormForm A)
(A,F) is Element of Normal_forms_on A
(A,O) \ (A,F) is finite Element of Fin (DISJOINT_PAIRS A)
sd . F is finite Element of Fin (DISJOINT_PAIRS A)
F is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
w is Element of the carrier of (NormForm A)
F . w is Element of the carrier of (NormForm A)
O \ w is Element of bool O
(A,w) is Element of Normal_forms_on A
sd is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
F is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
w is Element of the carrier of (NormForm A)
sd . w is Element of the carrier of (NormForm A)
O \ w is Element of bool O
F . w is Element of the carrier of (NormForm A)
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
O is Element of the carrier of (NormForm A)
(A,O) is finite Element of Fin the carrier of (NormForm A)
Fin the carrier of (NormForm A) is non empty cup-closed diff-closed preBoolean set
bool O is non empty cup-closed diff-closed preBoolean set
(A,O) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
sd is Element of the carrier of (NormForm A)
(A,O) . sd is Element of the carrier of (NormForm A)
sd "\/" ((A,O) . sd) is Element of the carrier of (NormForm A)
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
(A,O) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A,sd) is Element of Normal_forms_on A
(A,O) \ (A,sd) is finite Element of Fin (DISJOINT_PAIRS A)
(A,((A,O) . sd)) is Element of Normal_forms_on A
the L_join of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
H₁(A) . (sd,((A,O) . sd)) is Element of the carrier of (NormForm A)
(A,sd) \/ ((A,O) \ (A,sd)) is finite Element of Fin (DISJOINT_PAIRS A)
mi ((A,sd) \/ ((A,O) \ (A,sd))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,sd) \/ ((A,O) \ (A,sd)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,sd) \/ ((A,O) \ (A,sd)) & b₂ c= b₁ ) ) ) } is set
mi (A,O) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,O) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,O) & b₂ c= b₁ ) ) ) } is set
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
O is Element of the carrier of (NormForm A)
(A,O) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
sd is Element of the carrier of (NormForm A)
(A,O) . sd is Element of the carrier of (NormForm A)
O \ sd is Element of bool O
bool O is non empty cup-closed diff-closed preBoolean set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
F is Element of DISJOINT_PAIRS A
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
O is Element of DISJOINT_PAIRS A
(A,O) is non empty finite Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
sd is Element of the carrier of (NormForm A)
(A,sd) is finite Element of Fin the carrier of (NormForm A)
Fin the carrier of (NormForm A) is non empty cup-closed diff-closed preBoolean set
bool sd is non empty cup-closed diff-closed preBoolean set
(A,sd) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
{ H₃(b₁) where b₁ is Element of DISJOINT_PAIRS A : ( H₃(b₁) in sd & S₂[b₁] ) } is set
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : S₄[b₁] } is set
{ H₄(b₁) where b₁ is Element of DISJOINT_PAIRS A : ( b₁ in { b₁ where b₂ is Element of DISJOINT_PAIRS A : S₄[b₁] } & S₁[b₁] ) } is set
{ H₄(b₁) where b₁ is Element of DISJOINT_PAIRS A : ( S₄[b₁] & S₁[b₁] ) } is set
{ H₄(b₁) where b₁ is Element of DISJOINT_PAIRS A : S₄[b₁] } is set
w is set
pf is Element of DISJOINT_PAIRS A
pf \/ O is Element of [:(Fin A),(Fin A):]
pf `1 is finite Element of Fin A
O `1 is finite Element of Fin A
(pf `1) \/ (O `1) is finite Element of Fin A
pf `2 is finite Element of Fin A
O `2 is finite Element of Fin A
(pf `2) \/ (O `2) is finite Element of Fin A
[((pf `1) \/ (O `1)),((pf `2) \/ (O `2))] is V1() Element of [:(Fin A),(Fin A):]
{((pf `1) \/ (O `1)),((pf `2) \/ (O `2))} is non empty finite V27() set
{((pf `1) \/ (O `1))} is non empty finite V27() set
{{((pf `1) \/ (O `1)),((pf `2) \/ (O `2))},{((pf `1) \/ (O `1))}} is non empty finite V27() set
w is set
pf is Element of DISJOINT_PAIRS A
pf \/ O is Element of [:(Fin A),(Fin A):]
pf `1 is finite Element of Fin A
O `1 is finite Element of Fin A
(pf `1) \/ (O `1) is finite Element of Fin A
pf `2 is finite Element of Fin A
O `2 is finite Element of Fin A
(pf `2) \/ (O `2) is finite Element of Fin A
[((pf `1) \/ (O `1)),((pf `2) \/ (O `2))] is V1() Element of [:(Fin A),(Fin A):]
{((pf `1) \/ (O `1)),((pf `2) \/ (O `2))} is non empty finite V27() set
{((pf `1) \/ (O `1))} is non empty finite V27() set
{{((pf `1) \/ (O `1)),((pf `2) \/ (O `2))},{((pf `1) \/ (O `1))}} is non empty finite V27() set
w is Element of the carrier of (NormForm A)
(A,w) is Element of Normal_forms_on A
(A,w) ^ (A,O) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,w) & b₂ in (A,O) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,w) & b₂ in (A,O) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
(A,sd) . w is Element of the carrier of (NormForm A)
{ H₄(b₁) where b₁ is Element of DISJOINT_PAIRS A : b₁ in { b₁ where b₂ is Element of DISJOINT_PAIRS A : S₄[b₁] } } is set
pf is set
sf is Element of DISJOINT_PAIRS A
sf \/ O is Element of [:(Fin A),(Fin A):]
sf `1 is finite Element of Fin A
O `1 is finite Element of Fin A
(sf `1) \/ (O `1) is finite Element of Fin A
sf `2 is finite Element of Fin A
O `2 is finite Element of Fin A
(sf `2) \/ (O `2) is finite Element of Fin A
[((sf `1) \/ (O `1)),((sf `2) \/ (O `2))] is V1() Element of [:(Fin A),(Fin A):]
{((sf `1) \/ (O `1)),((sf `2) \/ (O `2))} is non empty finite V27() set
{((sf `1) \/ (O `1))} is non empty finite V27() set
{{((sf `1) \/ (O `1)),((sf `2) \/ (O `2))},{((sf `1) \/ (O `1))}} is non empty finite V27() set
pf is set
sf is Element of DISJOINT_PAIRS A
sf \/ O is Element of [:(Fin A),(Fin A):]
sf `1 is finite Element of Fin A
O `1 is finite Element of Fin A
(sf `1) \/ (O `1) is finite Element of Fin A
sf `2 is finite Element of Fin A
O `2 is finite Element of Fin A
(sf `2) \/ (O `2) is finite Element of Fin A
[((sf `1) \/ (O `1)),((sf `2) \/ (O `2))] is V1() Element of [:(Fin A),(Fin A):]
{((sf `1) \/ (O `1)),((sf `2) \/ (O `2))} is non empty finite V27() set
{((sf `1) \/ (O `1))} is non empty finite V27() set
{{((sf `1) \/ (O `1)),((sf `2) \/ (O `2))},{((sf `1) \/ (O `1))}} is non empty finite V27() set
{ H₅(b₁,b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₂ = O & S₅[b₁,b₂] ) } is set
{ H₅(b₁,O) where b₁ is Element of DISJOINT_PAIRS A : S₅[b₁,O] } is set
pf is Element of DISJOINT_PAIRS A
sf is Element of DISJOINT_PAIRS A
v is Element of DISJOINT_PAIRS A
a is Element of DISJOINT_PAIRS A
{ H₅(b₁,b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : S₆[b₁,b₂] } is set
{ H₅(b₁,b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : S₇[b₁,b₂] } is set
{ H₄(b₁) where b₁ is Element of DISJOINT_PAIRS A : ( S₃[b₁] & not H₄(b₁) in DISJOINT_PAIRS A ) } is set
pf is Element of DISJOINT_PAIRS A
pf \/ O is Element of [:(Fin A),(Fin A):]
pf `1 is finite Element of Fin A
O `1 is finite Element of Fin A
(pf `1) \/ (O `1) is finite Element of Fin A
pf `2 is finite Element of Fin A
O `2 is finite Element of Fin A
(pf `2) \/ (O `2) is finite Element of Fin A
[((pf `1) \/ (O `1)),((pf `2) \/ (O `2))] is V1() Element of [:(Fin A),(Fin A):]
{((pf `1) \/ (O `1)),((pf `2) \/ (O `2))} is non empty finite V27() set
{((pf `1) \/ (O `1))} is non empty finite V27() set
{{((pf `1) \/ (O `1)),((pf `2) \/ (O `2))},{((pf `1) \/ (O `1))}} is non empty finite V27() set
sd \ w is Element of bool sd
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
(A) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
Bottom (NormForm A) is Element of the carrier of (NormForm A)
O is Element of the carrier of (NormForm A)
(A) . O is Element of the carrier of (NormForm A)
O "/\" ((A) . O) is Element of the carrier of (NormForm A)
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A,((A) . O)) is Element of Normal_forms_on A
(A,O) is Element of Normal_forms_on A
(A,(A,O)) is finite Element of Fin (DISJOINT_PAIRS A)
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,O) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,O) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,O) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,O) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,O) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,O) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (A,(A,O)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,O)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,O)) & b₂ c= b₁ ) ) ) } is set
the L_meet of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
H₂(A) . (O,((A) . O)) is Element of the carrier of (NormForm A)
(A,O) ^ (mi (A,(A,O))) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,O) & b₂ in mi (A,(A,O)) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,O) & b₂ in mi (A,(A,O)) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi ((A,O) ^ (mi (A,(A,O)))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,O) ^ (mi (A,(A,O))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,O) ^ (mi (A,(A,O))) & b₂ c= b₁ ) ) ) } is set
(A,O) ^ (A,(A,O)) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,O) & b₂ in (A,(A,O)) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,O) & b₂ in (A,(A,O)) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi ((A,O) ^ (A,(A,O))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,O) ^ (A,(A,O)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,O) ^ (A,(A,O)) & b₂ c= b₁ ) ) ) } is set
sd is Element of Normal_forms_on A
mi sd is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in sd or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in sd & b₂ c= b₁ ) ) ) } is set
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
(A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
O is Element of the carrier of (NormForm A)
sd is Element of the carrier of (NormForm A)
(A) . (O,sd) is Element of the carrier of (NormForm A)
O "/\" ((A) . (O,sd)) is Element of the carrier of (NormForm A)
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
F is Element of DISJOINT_PAIRS A
(A,((A) . (O,sd))) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A,O) is Element of Normal_forms_on A
(A,sd) is Element of Normal_forms_on A
(A,(A,O),(A,sd)) is finite Element of Fin (DISJOINT_PAIRS A)
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) V11( DISJOINT_PAIRS A) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion ((A,O),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,O) c= (A,sd) } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion ((A,O),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,O) c= (A,sd) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (A,(A,O),(A,sd)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,O),(A,sd)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,O),(A,sd)) & b₂ c= b₁ ) ) ) } is set
the L_meet of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
H₂(A) . (O,((A) . (O,sd))) is Element of the carrier of (NormForm A)
(A,O) ^ (mi (A,(A,O),(A,sd))) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,O) & b₂ in mi (A,(A,O),(A,sd)) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,O) & b₂ in mi (A,(A,O),(A,sd)) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi ((A,O) ^ (mi (A,(A,O),(A,sd)))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,O) ^ (mi (A,(A,O),(A,sd))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,O) ^ (mi (A,(A,O),(A,sd))) & b₂ c= b₁ ) ) ) } is set
(A,O) ^ (A,(A,O),(A,sd)) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,O) & b₂ in (A,(A,O),(A,sd)) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,O) & b₂ in (A,(A,O),(A,sd)) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi ((A,O) ^ (A,(A,O),(A,sd))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,O) ^ (A,(A,O),(A,sd)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,O) ^ (A,(A,O),(A,sd)) & b₂ c= b₁ ) ) ) } is set
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
O is Element of DISJOINT_PAIRS A
(A,O) is non empty finite Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A) . O is Element of the carrier of (NormForm A)
sd is Element of the carrier of (NormForm A)
(A,sd) is Element of Normal_forms_on A
(A,sd) ^ (A,O) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,sd) & b₂ in (A,O) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,sd) & b₂ in (A,O) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
(A) . sd is Element of the carrier of (NormForm A)
F is Element of DISJOINT_PAIRS A
(A,(A,sd)) is finite Element of Fin (DISJOINT_PAIRS A)
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,sd) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,sd) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,sd) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,sd) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,sd) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,sd) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
w is Element of DISJOINT_PAIRS A
mi (A,(A,sd)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,sd)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,sd)) & b₂ c= b₁ ) ) ) } is set
pf is Element of DISJOINT_PAIRS A
sf is Element of DISJOINT_PAIRS A
A is set
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
O is Element of DISJOINT_PAIRS A
(A) . O is Element of the carrier of (NormForm A)
sd is Element of the carrier of (NormForm A)
sd "/\" ((A) . O) is Element of the carrier of (NormForm A)
F is Element of the carrier of (NormForm A)
(A) . (sd,F) is Element of the carrier of (NormForm A)
w is Element of DISJOINT_PAIRS A
w \/ O is Element of [:(Fin A),(Fin A):]
w `1 is finite Element of Fin A
O `1 is finite Element of Fin A
(w `1) \/ (O `1) is finite Element of Fin A
w `2 is finite Element of Fin A
O `2 is finite Element of Fin A
(w `2) \/ (O `2) is finite Element of Fin A
[((w `1) \/ (O `1)),((w `2) \/ (O `2))] is V1() Element of [:(Fin A),(Fin A):]
{((w `1) \/ (O `1)),((w `2) \/ (O `2))} is non empty finite V27() set
{((w `1) \/ (O `1))} is non empty finite V27() set
{{((w `1) \/ (O `1)),((w `2) \/ (O `2))},{((w `1) \/ (O `1))}} is non empty finite V27() set
(A,((A) . O)) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A,sd) is Element of Normal_forms_on A
(A,sd) ^ (A,((A) . O)) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,sd) & b₂ in (A,((A) . O)) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,sd) & b₂ in (A,((A) . O)) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi ((A,sd) ^ (A,((A) . O))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,sd) ^ (A,((A) . O)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,sd) ^ (A,((A) . O)) & b₂ c= b₁ ) ) ) } is set
pf is Element of DISJOINT_PAIRS A
the L_meet of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
H₂(A) . (sd,((A) . O)) is Element of the carrier of (NormForm A)
sf is Element of DISJOINT_PAIRS A
a is Element of DISJOINT_PAIRS A
w is Element of DISJOINT_PAIRS A
(A,F) is Element of Normal_forms_on A
(A,(A,sd),(A,F)) is finite Element of Fin (DISJOINT_PAIRS A)
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) V11( DISJOINT_PAIRS A) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion ((A,sd),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,sd) c= (A,F) } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion ((A,sd),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,sd) c= (A,F) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
pf is Element of DISJOINT_PAIRS A
mi (A,(A,sd),(A,F)) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,sd),(A,F)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,sd),(A,F)) & b₂ c= b₁ ) ) ) } is set
sf is Element of DISJOINT_PAIRS A
a is Element of DISJOINT_PAIRS A
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
the L_meet of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
O is Element of the carrier of (NormForm A)
(A,O) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
sd is Element of the carrier of (NormForm A)
(A) [:] ((A,O),sd) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
H₂(A) .: ((A),((A) [:] ((A,O),sd))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
w is Element of the carrier of (NormForm A)
(A,O) . w is Element of the carrier of (NormForm A)
(A) . w is Element of the carrier of (NormForm A)
(A) . (((A,O) . w),sd) is Element of the carrier of (NormForm A)
((A) . w) "/\" ((A) . (((A,O) . w),sd)) is Element of the carrier of (NormForm A)
w "/\" (((A) . w) "/\" ((A) . (((A,O) . w),sd))) is Element of the carrier of (NormForm A)
w "/\" ((A) . w) is Element of the carrier of (NormForm A)
(w "/\" ((A) . w)) "/\" ((A) . (((A,O) . w),sd)) is Element of the carrier of (NormForm A)
Bottom (NormForm A) is Element of the carrier of (NormForm A)
(Bottom (NormForm A)) "/\" ((A) . (((A,O) . w),sd)) is Element of the carrier of (NormForm A)
(A,O) is finite Element of Fin the carrier of (NormForm A)
Fin the carrier of (NormForm A) is non empty cup-closed diff-closed preBoolean set
bool O is non empty cup-closed diff-closed preBoolean set
w "\/" ((A,O) . w) is Element of the carrier of (NormForm A)
H₂(A) [;] (O,(H₂(A) .: ((A),((A) [:] ((A,O),sd))))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
(H₂(A) [;] (O,(H₂(A) .: ((A),((A) [:] ((A,O),sd)))))) . w is Element of the carrier of (NormForm A)
(H₂(A) .: ((A),((A) [:] ((A,O),sd)))) . w is Element of the carrier of (NormForm A)
H₂(A) . (O,((H₂(A) .: ((A),((A) [:] ((A,O),sd)))) . w)) is Element of the carrier of (NormForm A)
O "/\" ((H₂(A) .: ((A),((A) [:] ((A,O),sd)))) . w) is Element of the carrier of (NormForm A)
((A) [:] ((A,O),sd)) . w is Element of the carrier of (NormForm A)
H₂(A) . (((A) . w),(((A) [:] ((A,O),sd)) . w)) is Element of the carrier of (NormForm A)
O "/\" (H₂(A) . (((A) . w),(((A) [:] ((A,O),sd)) . w))) is Element of the carrier of (NormForm A)
((A) . w) "/\" (((A) [:] ((A,O),sd)) . w) is Element of the carrier of (NormForm A)
O "/\" (((A) . w) "/\" (((A) [:] ((A,O),sd)) . w)) is Element of the carrier of (NormForm A)
O "/\" (((A) . w) "/\" ((A) . (((A,O) . w),sd))) is Element of the carrier of (NormForm A)
((A,O) . w) "/\" (((A) . w) "/\" ((A) . (((A,O) . w),sd))) is Element of the carrier of (NormForm A)
(w "/\" (((A) . w) "/\" ((A) . (((A,O) . w),sd)))) "\/" (((A,O) . w) "/\" (((A) . w) "/\" ((A) . (((A,O) . w),sd)))) is Element of the carrier of (NormForm A)
((A) . (((A,O) . w),sd)) "/\" ((A) . w) is Element of the carrier of (NormForm A)
((A,O) . w) "/\" (((A) . (((A,O) . w),sd)) "/\" ((A) . w)) is Element of the carrier of (NormForm A)
((A,O) . w) "/\" ((A) . (((A,O) . w),sd)) is Element of the carrier of (NormForm A)
(((A,O) . w) "/\" ((A) . (((A,O) . w),sd))) "/\" ((A) . w) is Element of the carrier of (NormForm A)
FinJoin ((A,O),(H₂(A) .: ((A),((A) [:] ((A,O),sd))))) is Element of the carrier of (NormForm A)
O "/\" H₃(O,sd) is Element of the carrier of (NormForm A)
FinJoin ((A,O),(H₂(A) [;] (O,(H₂(A) .: ((A),((A) [:] ((A,O),sd))))))) is Element of the carrier of (NormForm A)
O "/\" sd is Element of the carrier of (NormForm A)
w is Element of the carrier of (NormForm A)
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
(A,sd) is Element of Normal_forms_on A
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set
bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
FinJoin ((A,sd),(A)) is Element of the carrier of (NormForm A)
H₂(A) [;] (O,(A)) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]
FinJoin ((A,sd),(H₂(A) [;] (O,(A)))) is Element of the carrier of (NormForm A)
(A) [:] ((A,O),w) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
a is Element of DISJOINT_PAIRS A
(H₂(A) [;] (O,(A))) . a is Element of the carrier of (NormForm A)
(A) . a is Element of the carrier of (NormForm A)
H₂(A) . (O,((A) . a)) is Element of the carrier of (NormForm A)
O "/\" ((A) . a) is Element of the carrier of (NormForm A)
(A,a) is non empty finite Element of Normal_forms_on A
v is Element of the carrier of (NormForm A)
(A,v) is Element of Normal_forms_on A
(A,v) ^ (A,a) is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,v) & b₂ in (A,a) ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in (A,v) & b₂ in (A,a) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
(A,O) . v is Element of the carrier of (NormForm A)
((A,O) . v) "/\" ((A) . a) is Element of the carrier of (NormForm A)
(A) . (((A,O) . v),w) is Element of the carrier of (NormForm A)
((A) [:] ((A,O),w)) . v is Element of the carrier of (NormForm A)
(A) . v is Element of the carrier of (NormForm A)
((A) . v) "/\" (((A) [:] ((A,O),w)) . v) is Element of the carrier of (NormForm A)
H₂(A) . (((A) . v),(((A) [:] ((A,O),w)) . v)) is Element of the carrier of (NormForm A)
H₂(A) .: ((A),((A) [:] ((A,O),w))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
(H₂(A) .: ((A),((A) [:] ((A,O),w)))) . v is Element of the carrier of (NormForm A)
FinJoin ((A,O),(H₂(A) .: ((A),((A) [:] ((A,O),w))))) is Element of the carrier of (NormForm A)
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
the carrier of (NormForm A) is non empty set
O is Element of the carrier of (NormForm A)
sd is Element of the carrier of (NormForm A)
(A,O) is finite Element of Fin the carrier of (NormForm A)
Fin the carrier of (NormForm A) is non empty cup-closed diff-closed preBoolean set
bool O is non empty cup-closed diff-closed preBoolean set
the L_meet of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
(A,O) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
(A) [:] ((A,O),sd) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
H₂(A) .: ((A),((A) [:] ((A,O),sd))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
FinJoin ((A,O),(H₂(A) .: ((A),((A) [:] ((A,O),sd))))) is Element of the carrier of (NormForm A)
F is Element of the carrier of (NormForm A)
O "/\" F is Element of the carrier of (NormForm A)
O "/\" F is Element of the carrier of (NormForm A)
w is Element of the carrier of (NormForm A)
O "/\" w is Element of the carrier of (NormForm A)
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded implicative Heyting LattStr
the carrier of (NormForm A) is non empty set
the L_meet of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
O is Element of the carrier of (NormForm A)
(A,O) is finite Element of Fin the carrier of (NormForm A)
Fin the carrier of (NormForm A) is non empty cup-closed diff-closed preBoolean set
bool O is non empty cup-closed diff-closed preBoolean set
(A,O) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
sd is Element of the carrier of (NormForm A)
O => sd is Element of the carrier of (NormForm A)
(A) [:] ((A,O),sd) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
the L_meet of (NormForm A) .: ((A),((A) [:] ((A,O),sd))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
FinJoin ((A,O),( the L_meet of (NormForm A) .: ((A),((A) [:] ((A,O),sd))))) is Element of the carrier of (NormForm A)
H₂(A) .: ((A),((A) [:] ((A,O),sd))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
FinJoin ((A,O),(H₂(A) .: ((A),((A) [:] ((A,O),sd))))) is Element of the carrier of (NormForm A)
O "/\" H₃(O,sd) is Element of the carrier of (NormForm A)
F is Element of the carrier of (NormForm A)
O "/\" F is Element of the carrier of (NormForm A)
A is set
NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded implicative Heyting LattStr
Top (NormForm A) is Element of the carrier of (NormForm A)
the carrier of (NormForm A) is non empty set
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
Fin A is non empty cup-closed diff-closed preBoolean set
[:(Fin A),(Fin A):] is non empty V7() set
bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Element of [:(Fin A),(Fin A):] : b₁ `1 misses b<sub>1</sub> `2 } is set
Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set
Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))
bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (DISJOINT_PAIRS A) : for b₂, b₃ being Element of DISJOINT_PAIRS A holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) } is set
(A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set
[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set
bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
Bottom (NormForm A) is Element of the carrier of (NormForm A)
(A,(Bottom (NormForm A))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
bool [: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set
(A) [:] ((A,(Bottom (NormForm A))),(Bottom (NormForm A))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
the L_meet of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
(A) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
H₂(A) .: ((A),((A) [:] ((A,(Bottom (NormForm A))),(Bottom (NormForm A))))) is non empty V7() V10( the carrier of (NormForm A)) V11( the carrier of (NormForm A)) Function-like V17( the carrier of (NormForm A)) quasi_total Element of bool [: the carrier of (NormForm A), the carrier of (NormForm A):]
(A) . (Bottom (NormForm A)) is Element of the carrier of (NormForm A)
(A,((A) . (Bottom (NormForm A)))) is Element of Normal_forms_on A
(A,(Bottom (NormForm A))) is Element of Normal_forms_on A
(A,(A,(Bottom (NormForm A)))) is finite Element of Fin (DISJOINT_PAIRS A)
(A) is non empty set
Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
{ [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,(Bottom (NormForm A))) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,(Bottom (NormForm A))) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,(Bottom (NormForm A))) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b₁ . b₂) where b₂ is Element of DISJOINT_PAIRS A : ( b₁ . b₂ in b₂ `2 & b<sub>2</sub> in (A,(Bottom (NormForm A))) ) } , { (b<sub>1</sub> . b<sub>2</sub>) where b<sub>2</sub> is Element of DISJOINT_PAIRS A : ( b<sub>1</sub> . b<sub>2</sub> in b<sub>2</sub> `1 & b₂ in (A,(Bottom (NormForm A))) ) } ] where b₁ is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b₂ being Element of DISJOINT_PAIRS A holds
( not b₂ in (A,(Bottom (NormForm A))) or b₁ . b₂ in (b₂ `1) \/ (b<sub>2</sub> `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (A,(A,(Bottom (NormForm A)))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,(Bottom (NormForm A)))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,(Bottom (NormForm A)))) & b₂ c= b₁ ) ) ) } is set
O is Element of Normal_forms_on A
mi O is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in O or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in O & b₂ c= b₁ ) ) ) } is set
(A,(Bottom (NormForm A))) . (Bottom (NormForm A)) is Element of the carrier of (NormForm A)
{} \ {} is empty non proper V7() non-empty empty-yielding finite finite-yielding V27() Element of bool {}
((A) [:] ((A,(Bottom (NormForm A))),(Bottom (NormForm A)))) . (Bottom (NormForm A)) is Element of the carrier of (NormForm A)
(A,(((A) [:] ((A,(Bottom (NormForm A))),(Bottom (NormForm A)))) . (Bottom (NormForm A)))) is Element of Normal_forms_on A
(A) . ((Bottom (NormForm A)),(Bottom (NormForm A))) is Element of the carrier of (NormForm A)
(A,(A,(Bottom (NormForm A))),(A,(Bottom (NormForm A)))) is finite Element of Fin (DISJOINT_PAIRS A)
Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]
(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]
[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set
[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]
[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion ((A,(Bottom (NormForm A))),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,(Bottom (NormForm A))) c= (A,(Bottom (NormForm A))) } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion ((A,(Bottom (NormForm A))),((A) .: (b₁,(incl (DISJOINT_PAIRS A)))))) where b₁ is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : b₁ .: (A,(Bottom (NormForm A))) c= (A,(Bottom (NormForm A))) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (A,(A,(Bottom (NormForm A))),(A,(Bottom (NormForm A)))) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in (A,(A,(Bottom (NormForm A))),(A,(Bottom (NormForm A)))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (A,(A,(Bottom (NormForm A))),(A,(Bottom (NormForm A)))) & b₂ c= b₁ ) ) ) } is set
(Bottom (NormForm A)) => (Bottom (NormForm A)) is Element of the carrier of (NormForm A)
(A,(Bottom (NormForm A))) is finite Element of Fin the carrier of (NormForm A)
Fin the carrier of (NormForm A) is non empty cup-closed diff-closed preBoolean set
bool (Bottom (NormForm A)) is non empty cup-closed diff-closed preBoolean set
FinJoin ((A,(Bottom (NormForm A))),(H₂(A) .: ((A),((A) [:] ((A,(Bottom (NormForm A))),(Bottom (NormForm A))))))) is Element of the carrier of (NormForm A)
the L_join of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]
H₁(A) $$ ((A,(Bottom (NormForm A))),(H₂(A) .: ((A),((A) [:] ((A,(Bottom (NormForm A))),(Bottom (NormForm A))))))) is Element of the carrier of (NormForm A)
(H₂(A) .: ((A),((A) [:] ((A,(Bottom (NormForm A))),(Bottom (NormForm A)))))) . (Bottom (NormForm A)) is Element of the carrier of (NormForm A)
H₂(A) . (((A) . (Bottom (NormForm A))),(((A) [:] ((A,(Bottom (NormForm A))),(Bottom (NormForm A)))) . (Bottom (NormForm A)))) is Element of the carrier of (NormForm A)
O ^ O is finite Element of Fin (DISJOINT_PAIRS A)
{ (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in O & b₂ in O ) } is set
(DISJOINT_PAIRS A) /\ { (b₁ \/ b₂) where b₁, b₂ is Element of DISJOINT_PAIRS A : ( b₁ in O & b₂ in O ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
mi (O ^ O) is Element of Normal_forms_on A
{ b₁ where b₁ is Element of DISJOINT_PAIRS A : for b₂ being Element of DISJOINT_PAIRS A holds
( ( not b₂ in O ^ O or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in O ^ O & b₂ c= b₁ ) ) ) } is set