:: HEYTING1 semantic presentation

1 is non empty set
{{},1} is non empty finite set
K162() is set

is non empty finite V27() set

A is non empty set
O is non empty set
[:A,O:] is non empty V7() 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

w is set
F . w is set
A is non empty 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),(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

O is finite Element of Fin ()
mi O is Element of Normal_forms_on A
Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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),(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 Element of Fin ()
F is Element of DISJOINT_PAIRS A
sd is finite Element of Fin ()
w is Element of DISJOINT_PAIRS A
{O} is non empty V7() V10( Fin A) V11( Fin A) finite Element of bool ()

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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),(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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()

A is 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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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

the carrier of () is non empty set
O is Element of the carrier of ()
DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

[:(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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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),(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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()
{ (b1 \/ b2) where b1, b2 is Element of DISJOINT_PAIRS A : ( b1 in O & b2 in O ) } is set
() /\ { (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),(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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()
w is Element of DISJOINT_PAIRS A
pf is Element of DISJOINT_PAIRS A
A is set

the carrier of () is non empty set
O is Element of the carrier of ()
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),(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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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),(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

the carrier of () is non empty set
[:(), the carrier of ():] is non empty V7() set
bool [:(), the carrier of ():] is non empty cup-closed diff-closed preBoolean set
singleton () is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(),():]

[:(),():] is non empty V7() set
bool [:(),():] is non empty cup-closed diff-closed preBoolean set
dom () is non empty V7() V10( Fin A) V11( Fin A) Element of bool ()

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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
() . F is finite Element of Fin ()
(A,F) is non empty finite Element of Normal_forms_on A
() . sd is set
sd is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
F is Element of DISJOINT_PAIRS A
sd . F is Element of the carrier of ()
(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 ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
sd is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
F is Element of DISJOINT_PAIRS A
O . F is Element of the carrier of ()
(A,F) is non empty finite Element of Normal_forms_on A

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()
A is 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

the carrier of () is non empty set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
[:(), the carrier of ():] is non empty V7() set
bool [:(), the carrier of ():] 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 ()
(A,sd) is non empty finite Element of Normal_forms_on A

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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),(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

the carrier of () is non empty set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
[:(), the carrier of ():] is non empty V7() set
bool [:(), the carrier of ():] is non empty cup-closed diff-closed preBoolean set
O is Element of DISJOINT_PAIRS A
(A) . O is Element of the carrier of ()
(A,O) is non empty finite Element of Normal_forms_on A

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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),(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

the carrier of () is non empty set
(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
[:(), the carrier of ():] is non empty V7() set
bool [:(), the carrier of ():] is non empty cup-closed diff-closed preBoolean set

singleton () is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(),():]
[:(),():] is non empty V7() set
bool [:(),():] is non empty cup-closed diff-closed preBoolean set
O is Element of DISJOINT_PAIRS A
(A) . O is Element of the carrier of ()
() . O is finite Element of Fin ()
(A,O) is non empty finite Element of Normal_forms_on A
Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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),(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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
the carrier of () is non empty set
[:(), the carrier of ():] is non empty V7() set
bool [:(), the carrier of ():] is non empty cup-closed diff-closed preBoolean set
singleton () is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(),():]
[:(),():] is non empty V7() set
bool [:(),():] 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 ()
FinUnion (O,()) is finite Element of Fin ()
mi (FinUnion (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 FinUnion (O,()) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in FinUnion (O,()) & b2 c= b1 ) ) )
}
is set

sd is Element of DISJOINT_PAIRS A
F is Element of DISJOINT_PAIRS A
() . F is finite Element of Fin ()
w is Element of DISJOINT_PAIRS A
pf is Element of DISJOINT_PAIRS A
() . pf is finite Element of Fin ()
[:(),():] is non empty V7() set
bool [:(),():] is non empty cup-closed diff-closed preBoolean set
sd is non empty V7() V10( Fin ()) V11( Normal_forms_on A) Function-like V17( Fin ()) quasi_total Element of bool [:(),():]
[:(), the carrier of ():] is non empty V7() set
bool [:(), the carrier of ():] is non empty cup-closed diff-closed preBoolean set
F is non empty V7() V10( Fin ()) V11( the carrier of ()) Function-like V17( Fin ()) quasi_total Element of bool [:(), the carrier of ():]

F . () is Element of the carrier of ()
mi () 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 {}. () or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in {}. () & b2 c= b1 ) ) )
}
is set

Bottom () is Element of the carrier of ()
the L_join of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty V7() set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty cup-closed diff-closed preBoolean set
the_unity_wrt the L_join of () is Element of the carrier of ()
w is finite Element of Fin ()
F . w is Element of the carrier of ()
(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 ()
F . pf is Element of the carrier of ()
(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 ()
F . (w \/ pf) is Element of the carrier of ()
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 ()
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 ()
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 () . ((F . w),(F . pf)) is Element of the carrier of ()
F * () is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
w is Element of DISJOINT_PAIRS A
(F * ()) . w is Element of the carrier of ()
() . w is finite Element of Fin ()
F . (() . w) is Element of the carrier of ()
(A,w) is non empty finite Element of Normal_forms_on A
F . (A,w) is Element of the carrier of ()
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 ()
the L_join of () \$\$ (O,(A)) is Element of the carrier of ()
the L_join of () \$\$ (O,(F * ())) is Element of the carrier of ()
F . (FinUnion (O,())) is Element of the carrier of ()
A is set

the carrier of () 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),(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 ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(), the carrier of ():]
[:(), the carrier of ():] is non empty V7() set
bool [:(), the carrier of ():] is non empty cup-closed diff-closed preBoolean set
O is Element of the carrier of ()
(A,O) is Element of Normal_forms_on A

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()
singleton () is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin ()) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(),():]
[:(),():] is non empty V7() set
bool [:(),():] is non empty cup-closed diff-closed preBoolean set
FinUnion ((A,O),()) is finite Element of Fin ()
A is set

the carrier of () is non empty 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 ()
sd is Element of the carrier of ()
O "\/" sd is Element of the carrier of ()
the L_join of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty V7() set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty cup-closed diff-closed preBoolean set
the L_join of () . (O,sd) is Element of the carrier of ()
(A,O) is Element of Normal_forms_on A

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()
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

the carrier of () is non empty 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 ()
sd is Element of the carrier of ()
(A,O) is Element of Normal_forms_on A

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()
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 ()
the L_join of () is non empty V7() V10([: the carrier of (), the carrier of ():]) V11( the carrier of ()) Function-like V17([: the carrier of (), the carrier of ():]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty V7() set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty V7() set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty cup-closed diff-closed preBoolean set
the L_join of () . (O,sd) is Element of the carrier of ()
A is 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),(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 set
Funcs ((),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
O is finite Element of Fin ()
{ [ { (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 ((),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `2) )
}
is set

() /\ { [ { (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 ((),(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 ((),(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 ((),(A)) : b1 .: O c= union { ((b1 `1) \/ (b1 `2)) where b2 is Element of DISJOINT_PAIRS A : b1 in O } } 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 ((),(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 ((),(A))
sf is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((),(A))
pf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11((A)) Function-like finite Element of bool [:(),(A):]
[:(),(A):] is non empty V7() set
bool [:(),(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 [:(),(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 ((),(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 ()

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 ((),(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 ((),(A)) : S1[b1] } is set
{ H1(b1) where b1 is Element of DISJOINT_PAIRS A : b1 in O } is set
Funcs ((),[:(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 () 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 [:(),[:(Fin A),(Fin A):]:]
[:(),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
sd is finite Element of Fin ()
{ (FinPairUnion (O,((A) .: (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 ((),[:(Fin A),(Fin A):]) : b1 .: O c= sd } is set
() /\ { (FinPairUnion (O,((A) .: (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 ((),[:(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 ((),[:(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 [:(),[:(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 ((),[:(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 [:(),[:(Fin A),(Fin A):]:]
(A) .: (pf,()) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(),[:(Fin A),(Fin A):]:]
((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 [:(),[:(Fin A),(Fin A):]:]
(A) .: (sf,()) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(),[:(Fin A),(Fin A):]:]
((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 [:(),[:(Fin A),(Fin A):]:]
FinPairUnion (O,((A) .: (pf,()))) 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):]:]
() \$\$ (O,((A) .: (pf,()))) is Element of [:(Fin A),(Fin A):]
FinPairUnion (O,((A) .: (sf,()))) is Element of [:(Fin A),(Fin A):]
() \$\$ (O,((A) .: (sf,()))) 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 ((),[:(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),(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 set
Funcs ((),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)
O is finite Element of Fin ()
(A,O) is finite Element of Fin ()
{ [ { (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 ((),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `2) )
}
is set

() /\ { [ { (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 ((),(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 ((),(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),(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),({}. 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),(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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()
(A) is non empty set
Funcs ((),(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 ((),(A)) : for b2 being Element of DISJOINT_PAIRS A holds
( not b2 in O or b1 . b2 in (b2 `1) \/ (b2 `2) )
}
is set

() /\ { [ { (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 ((),(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 ((),(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 ((),(A)) is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((),(A))
F is set
{ ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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 ((),(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),(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

Normal_forms_on A is non empty Element of bool ()
bool () is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is finite Element of Fin () : 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 ()
Funcs ((),[:(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 () 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 [:(),[:(Fin A),(Fin A):]:]
[:(),[:(Fin A),(Fin A):]:] is non empty V7() set
bool [:(),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set
{ (FinPairUnion (O,((A) .: (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 ((),[:(Fin A),(Fin A):]) : b1 .: O c= sd } is set
() /\ { (FinPairUnion (O,((A) .: (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 ((),[:(Fin A),(Fin A):]) : b1 .: O c= sd } is V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

F is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((),[:(Fin A),(Fin A):])
(A) .: (F,()) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(),[:(Fin A),(Fin A):]:]
FinPairUnion (O,((A) .: (F,()))) 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):]:]
() \$\$ (O,((A) .: (F,()))) is Element of [:(Fin A),(Fin A):]
the_unity_wrt () 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 ((),[:(Fin A),(Fin A):])
(A) .: (w,()) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(),[:(Fin A),(Fin A):]:]
FinPairUnion (O,((A) .: (w,()))) is Element of [:(Fin A),(Fin A):]
() \$\$ (O,((A) .: (w,()))) 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 ((),[:(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 ((),[:(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 ((),[:(Fin A),(Fin 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 [:(),[:(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 ((),[:(Fin A),(Fin A):]),()))) is Element of [:(Fin A),(Fin 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 ((),[:(Fin A),(Fin 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 ((),[:(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
[:(),():] is non empty V7() set
DISJOINT_PAIRS {} is non empty V7() V10( Fin {}) V11( Fin {}) Element of bool [:(),():]
bool [:(),():] is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is Element of [:(),()<