{} 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } is set
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in O or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in O & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } is set
O is Element of Normal_forms_on A
O ^ O is finite Element of Fin (DISJOINT_PAIRS A)
{ (b1 \/ b2) where b1, b2 is Element of DISJOINT_PAIRS A : ( b1 in O & b2 in O ) } is set
(DISJOINT_PAIRS A) /\ { (b1 \/ b2) where b1, b2 is Element of DISJOINT_PAIRS A : ( b1 in O & b2 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in O ^ O or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in O ^ O & b2 c= b1 ) ) ) } is set
mi O is Element of Normal_forms_on A
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in O or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in O & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in FinUnion (O,(singleton (DISJOINT_PAIRS A))) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in FinUnion (O,(singleton (DISJOINT_PAIRS A))) & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in {}. (DISJOINT_PAIRS A) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in {}. (DISJOINT_PAIRS A) & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in w or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in w & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in pf or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in pf & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in w \/ pf or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in w \/ pf & b2 c= b1 ) ) ) } is set
(mi w) \/ pf is finite Element of Fin (DISJOINT_PAIRS A)
mi ((mi w) \/ pf) is Element of Normal_forms_on A
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in (mi w) \/ pf or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (mi w) \/ pf & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in (mi w) \/ (mi pf) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (mi w) \/ (mi pf) & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in (A,w) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (A,w) & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in (A,O) \/ (A,sd) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (A,O) \/ (A,sd) & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in (A,O) \/ (A,sd) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (A,O) \/ (A,sd) & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of DISJOINT_PAIRS A : for b2 being Element of DISJOINT_PAIRS A holds
( ( not b2 in (A,sd) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (A,sd) & b2 c= b1 ) ) ) } 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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)
{ [ { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `2 & b2 in O ) } , { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `1 & b2 in O ) } ] where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `2 & b2 in O ) } , { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `1 & b2 in O ) } ] where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `2) ) } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]
{ ((b1 `1) \/ (b1 `2)) where b1 is Element of DISJOINT_PAIRS A : b1 in O } is set
union { ((b1 `1) \/ (b1 `2)) where b1 is Element of DISJOINT_PAIRS A : b1 in O } is set
{ (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `2 & b1 in O ) } is set
{ (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `1 & b1 in O ) } is set
[ { (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `2 & b1 in O ) } , { (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `1 & b1 in O ) } ] is V1() set
{ { (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `2 & b1 in O ) } , { (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `1 & b1 in O ) } } is non empty finite set
{ { (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `2 & b1 in O ) } } is non empty finite set
{{ { (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `2 & b1 in O ) } , { (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `1 & b1 in O ) } },{ { (a1 . b1) where b1 is Element of DISJOINT_PAIRS A : ( a1 . b1 in b1 `2 & b1 in O ) } }} is non empty finite V27() set
{ H2(b1) where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `2) ) } is set
{ H2(b1) where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : b1 .: O c= union { ((b1 `1) \/ (b1 `2)) where b2 is Element of DISJOINT_PAIRS A : b1 in O } } is set
(DISJOINT_PAIRS A) /\ { H2(b1) where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `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 . b1) where b1 is Element of DISJOINT_PAIRS A : ( S3[b1] & b1 in O ) } is set
{ (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( S5[b1] & b1 in O ) } is set
a is Element of DISJOINT_PAIRS A
pf . a is set
a `2 is set
sf . a is set
{ (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( S4[b1] & b1 in O ) } is set
{ (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( S6[b1] & b1 in O ) } is set
{ (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `2 & b1 in O ) } is set
{ (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `1 & b1 in O ) } is set
[ { (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `2 & b1 in O ) } , { (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `1 & b1 in O ) } ] is V1() set
{ { (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `2 & b1 in O ) } , { (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `1 & b1 in O ) } } is non empty finite set
{ { (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `2 & b1 in O ) } } is non empty finite set
{{ { (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `2 & b1 in O ) } , { (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `1 & b1 in O ) } },{ { (pf . b1) where b1 is Element of DISJOINT_PAIRS A : ( pf . b1 in b1 `2 & b1 in O ) } }} is non empty finite V27() set
{ (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `2 & b1 in O ) } is set
{ (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `1 & b1 in O ) } is set
[ { (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `2 & b1 in O ) } , { (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `1 & b1 in O ) } ] is V1() set
{ { (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `2 & b1 in O ) } , { (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `1 & b1 in O ) } } is non empty finite set
{ { (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `2 & b1 in O ) } } is non empty finite set
{{ { (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `2 & b1 in O ) } , { (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `1 & b1 in O ) } },{ { (sf . b1) where b1 is Element of DISJOINT_PAIRS A : ( sf . b1 in b1 `2 & b1 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)
{ H2(b1) where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : S2[b1] } is set
{ H2(b1) where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : S1[b1] } is set
{ H1(b1) where b1 is Element of DISJOINT_PAIRS A : b1 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) .: (b1,(incl (DISJOINT_PAIRS A)))))) where b1 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):]) : b1 .: O c= sd } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion (O,((A) .: (b1,(incl (DISJOINT_PAIRS A)))))) where b1 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):]) : b1 .: 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):]
{ H1(b1) where b1 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):]) : b1 .: 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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)
{ [ { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `2 & b2 in O ) } , { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `1 & b2 in O ) } ] where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `2 & b2 in O ) } , { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `1 & b2 in O ) } ] where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `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 . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } is set
{ (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `1 & b1 in O ) } is set
[ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } , { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `1 & b1 in O ) } ] is V1() set
{ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } , { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `1 & b1 in O ) } } is non empty finite set
{ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } } is non empty finite set
{{ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } , { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `1 & b1 in O ) } },{ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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)
{ [ { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `2 & b2 in O ) } , { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `1 & b2 in O ) } ] where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `2) ) } is set
(DISJOINT_PAIRS A) /\ { [ { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `2 & b2 in O ) } , { (b1 . b2) where b2 is Element of DISJOINT_PAIRS A : ( b1 . b2 in b2 `1 & b2 in O ) } ] where b1 is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `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 . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } is set
{ (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `1 & b1 in O ) } is set
[ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } , { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `1 & b1 in O ) } ] is V1() set
{ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } , { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `1 & b1 in O ) } } is non empty finite set
{ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } } is non empty finite set
{{ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 in O ) } , { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `1 & b1 in O ) } },{ { (F . b1) where b1 is Element of DISJOINT_PAIRS A : ( F . b1 in b1 `2 & b1 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)) . b1) where b1 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)) . b1 in b1 `2 & b1 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)) . b1) where b1 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)) . b1 in b1 `2 & b1 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)) . b1) where b1 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)) . b1 in b1 `2 & b1 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)) . b1) where b1 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)) . b1 in b1 `1 & b1 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)) . b1) where b1 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)) . b1 in b1 `1 & b1 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)) . b1) where b1 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)) . b1 in b1 `1 & b1 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
{ b1 where b1 is Element of [:(Fin A),(Fin A):] : b1 `1 misses b1 `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
{ b1 where b1 is finite Element of Fin (DISJOINT_PAIRS A) : for b2, b3 being Element of DISJOINT_PAIRS A holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) } 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) .: (b1,(incl (DISJOINT_PAIRS A)))))) where b1 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):]) : b1 .: O c= sd } is set
(DISJOINT_PAIRS A) /\ { (FinPairUnion (O,((A) .: (b1,(incl (DISJOINT_PAIRS A)))))) where b1 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):]) : b1 .: 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
{ b1 where b1 is Element of [:(Fin {}),(Fin {})<