:: ORDERS_1 semantic presentation

{} is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set

the empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set

O is set

union O is set

A is set

the Element of A is Element of A

the Element of union O is Element of union O

g is set

O is non empty set

union O is set

[:O,(union O):] is Relation-like set

bool [:O,(union O):] is non empty set

the Element of O is Element of O

g is Relation-like Function-like set

dom g is set

rng g is set

ff is set

AA is non empty set

Y is set

z is set

g . z is set

{z} is non empty finite set

[:{z},z:] is Relation-like set

ff /\ Y is set

the Element of ff /\ Y is Element of ff /\ Y

AA9 is set

g . AA9 is set

{AA9} is non empty finite set

[:{AA9},AA9:] is Relation-like set

{AA9} /\ {z} is finite set

AA9 /\ z is set

f9 is set

x is set

[f9,x] is V35() set

{f9,x} is non empty finite set

{f9} is non empty finite set

{{f9,x},{f9}} is non empty finite V45() set

ff is set

Y is set

g . Y is set

{Y} is non empty finite set

[:{Y},Y:] is Relation-like set

ff is set

Y is set

Y /\ ff is set

ff /\ Y is set

z is set

{z} is non empty finite set

Y is set

Y /\ ff is set

z is set

y is set

ff /\ Y is set

AA9 is set

{AA9} is non empty finite set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

union AA is set

z is set

y is set

Y . y is set

y /\ ff is set

g . the Element of O is set

z is set

y is set

g . y is set

[:O,AA:] is non empty Relation-like set

bool [:O,AA:] is non empty set

f9 is Relation-like Function-like set

dom f9 is set

rng f9 is set

x is set

y is set

f9 . y is set

z is set

AA9 is non empty Relation-like O -defined AA -valued Function-like total V38(O,AA) Element of bool [:O,AA:]

dom AA9 is non empty Element of bool O

bool O is non empty set

a is set

AA9 . a is set

{a} is non empty finite set

[:{a},a:] is Relation-like set

P2 is set

y9 is set

[P2,y9] is V35() set

{P2,y9} is non empty finite set

{P2} is non empty finite set

{{P2,y9},{P2}} is non empty finite V45() set

[P2,y9] `2 is set

{y} is non empty finite set

[:{y},y:] is Relation-like set

[:AA,(union AA):] is Relation-like set

bool [:AA,(union AA):] is non empty set

[:(union AA),(union O):] is Relation-like set

bool [:(union AA),(union O):] is non empty set

AA9 is non empty Relation-like O -defined AA -valued Function-like total V38(O,AA) Element of bool [:O,AA:]

x is Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) Element of bool [:AA,(union AA):]

x * AA9 is Relation-like O -defined union AA -valued Function-like V38(O, union AA) Element of bool [:O,(union AA):]

[:O,(union AA):] is Relation-like set

bool [:O,(union AA):] is non empty set

dom (x * AA9) is Element of bool O

bool O is non empty set

y is Relation-like union AA -defined union O -valued Function-like V38( union AA, union O) Element of bool [:(union AA),(union O):]

y * (x * AA9) is Relation-like O -defined union O -valued Function-like Element of bool [:O,(union O):]

z is Relation-like O -defined union O -valued Function-like V38(O, union O) Element of bool [:O,(union O):]

a is set

z . a is set

AA9 . a is set

{a} is non empty finite set

[:{a},a:] is Relation-like set

x . (AA9 . a) is set

rng x is Element of bool (union AA)

bool (union AA) is non empty set

y . (x . (AA9 . a)) is set

(x . (AA9 . a)) `2 is set

(AA9 . a) /\ ff is set

y9 is set

z is set

[y9,z] is V35() set

{y9,z} is non empty finite set

{y9} is non empty finite set

{{y9,z},{y9}} is non empty finite V45() set

(x * AA9) . a is set

O is set

bool O is non empty set

bool O is non empty Element of bool (bool O)

bool (bool O) is non empty set

{{}} is non empty functional finite V45() set

(bool O) \ {{}} is Element of bool (bool O)

O is non empty set

(O) is set

bool O is non empty set

bool O is non empty Element of bool (bool O)

bool (bool O) is non empty set

(bool O) \ {{}} is Element of bool (bool O)

O is non empty set

(O) is non empty set

bool O is non empty set

bool O is non empty Element of bool (bool O)

bool (bool O) is non empty set

(bool O) \ {{}} is Element of bool (bool O)

O is set

(O) is set

bool O is non empty set

bool O is non empty Element of bool (bool O)

bool (bool O) is non empty set

(bool O) \ {{}} is Element of bool (bool O)

A is non empty set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued total V38(O,O) Element of bool [:O,O:]

field A is set

dom A is set

rng A is set

(dom A) \/ (rng A) is set

rng A is Element of bool O

bool O is non empty set

O \/ (rng A) is set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is set

[A,A] is V35() set

{A,A} is non empty finite set

{A} is non empty finite set

{{A,A},{A}} is non empty finite V45() set

g is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

field g is set

dom g is set

rng g is set

(dom g) \/ (rng g) is set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

AA is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

field AA is set

dom AA is set

rng AA is set

(dom AA) \/ (rng AA) is set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[A,AA] is V35() set

{A,AA} is non empty finite set

{{A,AA},{A}} is non empty finite V45() set

ff is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

field ff is set

dom ff is set

rng ff is set

(dom ff) \/ (rng ff) is set

A is set

O is set

union O is set

g is set

union g is set

O is set

A is Relation-like set

g is set

[g,g] is V35() set

{g,g} is non empty finite set

{g} is non empty finite set

{{g,g},{g}} is non empty finite V45() set

g is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[AA,g] is V35() set

{AA,g} is non empty finite set

{AA} is non empty finite set

{{AA,g},{AA}} is non empty finite V45() set

g is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[AA,g] is V35() set

{AA,g} is non empty finite set

{AA} is non empty finite set

{{AA,g},{AA}} is non empty finite V45() set

O is set

A is set

g is Relation-like set

AA is set

[AA,AA] is V35() set

{AA,AA} is non empty finite set

{AA} is non empty finite set

{{AA,AA},{AA}} is non empty finite V45() set

O is set

A is set

g is Relation-like set

AA is set

ff is set

[AA,ff] is V35() set

{AA,ff} is non empty finite set

{AA} is non empty finite set

{{AA,ff},{AA}} is non empty finite V45() set

[ff,AA] is V35() set

{ff,AA} is non empty finite set

{ff} is non empty finite set

{{ff,AA},{ff}} is non empty finite V45() set

O is set

A is set

g is Relation-like set

AA is set

ff is set

[AA,ff] is V35() set

{AA,ff} is non empty finite set

{AA} is non empty finite set

{{AA,ff},{AA}} is non empty finite V45() set

Y is set

[ff,Y] is V35() set

{ff,Y} is non empty finite set

{ff} is non empty finite set

{{ff,Y},{ff}} is non empty finite V45() set

[AA,Y] is V35() set

{AA,Y} is non empty finite set

{{AA,Y},{AA}} is non empty finite V45() set

O is set

A is set

g is Relation-like set

AA is set

ff is set

[AA,ff] is V35() set

{AA,ff} is non empty finite set

{AA} is non empty finite set

{{AA,ff},{AA}} is non empty finite V45() set

[ff,AA] is V35() set

{ff,AA} is non empty finite set

{ff} is non empty finite set

{{ff,AA},{ff}} is non empty finite V45() set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued total V38(O,O) Element of bool [:O,O:]

field A is set

dom A is set

rng A is set

(dom A) \/ (rng A) is set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued Element of bool [:O,O:]

dom A is Element of bool O

bool O is non empty set

field A is set

dom A is set

rng A is set

(dom A) \/ (rng A) is set

g is set

[g,g] is V35() set

{g,g} is non empty finite set

{g} is non empty finite set

{{g,g},{g}} is non empty finite V45() set

rng A is Element of bool O

O \/ (rng A) is set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

dom A is Element of bool O

bool O is non empty set

rng A is Element of bool O

g is set

[g,g] is V35() set

{g,g} is non empty finite set

{g} is non empty finite set

{{g,g},{g}} is non empty finite V45() set

g is set

[g,g] is V35() set

{g,g} is non empty finite set

{g} is non empty finite set

{{g,g},{g}} is non empty finite V45() set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

field A is set

dom A is set

rng A is set

(dom A) \/ (rng A) is set

O \/ O is set

dom A is Element of bool O

bool O is non empty set

(dom A) \/ O is set

O is Relation-like set

O ~ is Relation-like set

O is Relation-like set

O ~ is Relation-like set

O is Relation-like set

O ~ is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

A is set

field (O ~) is set

dom (O ~) is set

rng (O ~) is set

(dom (O ~)) \/ (rng (O ~)) is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

O is Relation-like set

O is Relation-like set

O is Relation-like set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

O is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

[:(field O),(field O):] is Relation-like set

A is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

O is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

field (O |_2 A) is set

dom (O |_2 A) is set

rng (O |_2 A) is set

(dom (O |_2 A)) \/ (rng (O |_2 A)) is set

g is set

g is set

[g,g] is V35() set

{g,g} is non empty finite set

{g} is non empty finite set

{{g,g},{g}} is non empty finite V45() set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

O is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set

field O is finite set

dom O is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set

rng O is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set

(dom O) \/ (rng O) is Relation-like reflexive irreflexive symmetric finite V45() set

O is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

[A,A] is V35() set

{A,A} is non empty finite set

{A} is non empty finite set

{{A,A},{A}} is non empty finite V45() set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[A,AA] is V35() set

{A,AA} is non empty finite set

{{A,AA},{A}} is non empty finite V45() set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

O is set

id O is Relation-like O -defined O -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V38(O,O) V39(O) V40(O,O) Element of bool [:O,O:]

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

O is Relation-like set

A is set

O is Relation-like set

A is set

O is Relation-like set

A is set

O is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

O is Relation-like set

A is set

g is set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

g is set

field (O |_2 A) is set

dom (O |_2 A) is set

rng (O |_2 A) is set

(dom (O |_2 A)) \/ (rng (O |_2 A)) is set

[g,g] is V35() set

{g,g} is non empty finite set

{g} is non empty finite set

{{g,g},{g}} is non empty finite V45() set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

g is set

field (O |_2 A) is set

dom (O |_2 A) is set

rng (O |_2 A) is set

(dom (O |_2 A)) \/ (rng (O |_2 A)) is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

ff is set

[AA,ff] is V35() set

{AA,ff} is non empty finite set

{AA} is non empty finite set

{{AA,ff},{AA}} is non empty finite V45() set

[g,ff] is V35() set

{g,ff} is non empty finite set

{{g,ff},{g}} is non empty finite V45() set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

g is set

field (O |_2 A) is set

dom (O |_2 A) is set

rng (O |_2 A) is set

(dom (O |_2 A)) \/ (rng (O |_2 A)) is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[AA,g] is V35() set

{AA,g} is non empty finite set

{AA} is non empty finite set

{{AA,g},{AA}} is non empty finite V45() set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

g is set

field (O |_2 A) is set

dom (O |_2 A) is set

rng (O |_2 A) is set

(dom (O |_2 A)) \/ (rng (O |_2 A)) is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[AA,g] is V35() set

{AA,g} is non empty finite set

{AA} is non empty finite set

{{AA,g},{AA}} is non empty finite V45() set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

O is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

O is Relation-like set

A is set

g is set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

O is Relation-like set

A is set

g is set

AA is set

ff is set

[AA,ff] is V35() set

{AA,ff} is non empty finite set

{AA} is non empty finite set

{{AA,ff},{AA}} is non empty finite V45() set

[ff,AA] is V35() set

{ff,AA} is non empty finite set

{ff} is non empty finite set

{{ff,AA},{ff}} is non empty finite V45() set

O is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

O is Relation-like set

A is set

g is set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

O is Relation-like set

O ~ is Relation-like set

A is set

g is set

[g,g] is V35() set

{g,g} is non empty finite set

{g} is non empty finite set

{{g,g},{g}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

g is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

ff is set

[AA,ff] is V35() set

{AA,ff} is non empty finite set

{AA} is non empty finite set

{{AA,ff},{AA}} is non empty finite V45() set

[g,ff] is V35() set

{g,ff} is non empty finite set

{{g,ff},{g}} is non empty finite V45() set

[ff,AA] is V35() set

{ff,AA} is non empty finite set

{ff} is non empty finite set

{{ff,AA},{ff}} is non empty finite V45() set

[AA,g] is V35() set

{AA,g} is non empty finite set

{{AA,g},{AA}} is non empty finite V45() set

[ff,g] is V35() set

{ff,g} is non empty finite set

{{ff,g},{ff}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

g is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[AA,g] is V35() set

{AA,g} is non empty finite set

{AA} is non empty finite set

{{AA,g},{AA}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

g is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[AA,g] is V35() set

{AA,g} is non empty finite set

{AA} is non empty finite set

{{AA,g},{AA}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

O is Relation-like set

O ~ is Relation-like set

A is set

O is Relation-like set

O ~ is Relation-like set

A is set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

field A is set

dom A is set

rng A is set

(dom A) \/ (rng A) is set

O is set

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]

field A is set

dom A is set

rng A is set

(dom A) \/ (rng A) is set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

bool [:A,A:] is non empty set

field (O |_2 A) is set

dom (O |_2 A) is set

rng (O |_2 A) is set

(dom (O |_2 A)) \/ (rng (O |_2 A)) is set

ff is set

Y is set

[ff,Y] is V35() set

{ff,Y} is non empty finite set

{ff} is non empty finite set

{{ff,Y},{ff}} is non empty finite V45() set

[Y,ff] is V35() set

{Y,ff} is non empty finite set

{Y} is non empty finite set

{{Y,ff},{Y}} is non empty finite V45() set

ff is set

Y is set

[ff,Y] is V35() set

{ff,Y} is non empty finite set

{ff} is non empty finite set

{{ff,Y},{ff}} is non empty finite V45() set

z is set

[Y,z] is V35() set

{Y,z} is non empty finite set

{Y} is non empty finite set

{{Y,z},{Y}} is non empty finite V45() set

[ff,z] is V35() set

{ff,z} is non empty finite set

{{ff,z},{ff}} is non empty finite V45() set

ff is set

[ff,ff] is V35() set

{ff,ff} is non empty finite set

{ff} is non empty finite set

{{ff,ff},{ff}} is non empty finite V45() set

AA is Relation-like A -defined A -valued Element of bool [:A,A:]

field AA is set

dom AA is set

rng AA is set

(dom AA) \/ (rng AA) is set

dom AA is Element of bool A

bool A is non empty set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

bool [:A,A:] is non empty set

O is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

bool [:A,A:] is non empty set

O is set

id O is Relation-like O -defined O -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V38(O,O) V39(O) V40(O,O) () () Element of bool [:O,O:]

[:O,O:] is Relation-like set

bool [:O,O:] is non empty set

field (id O) is set

dom (id O) is set

rng (id O) is set

(dom (id O)) \/ (rng (id O)) is set

rng (id O) is Element of bool O

bool O is non empty set

O \/ (rng (id O)) is set

O \/ O is set

O is Relation-like set

O ~ is Relation-like set

A is set

O |_2 A is Relation-like set

[:A,A:] is Relation-like set

O /\ [:A,A:] is Relation-like set

(O |_2 A) ~ is Relation-like set

(O ~) |_2 A is Relation-like set

(O ~) /\ [:A,A:] is Relation-like set

g is set

AA is set

[g,AA] is V35() set

{g,AA} is non empty finite set

{g} is non empty finite set

{{g,AA},{g}} is non empty finite V45() set

[AA,g] is V35() set

{AA,g} is non empty finite set

{AA} is non empty finite set

{{AA,g},{AA}} is non empty finite V45() set

O is Relation-like set

O |_2 {} is Relation-like set

[:{},{}:] is Relation-like finite set

O /\ [:{},{}:] is Relation-like finite set

{} |` O is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set

({} |` O) | {} is empty Relation-like non-empty empty-yielding rng ({} |` O) -valued reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set

rng ({} |` O) is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set

O is Relation-like set

A is set

O |_2 {} is Relation-like set

O /\ [:{},{}:] is Relation-like finite set

g is set

O is Relation-like set

A is set

O |_2 {} is Relation-like set

O /\ [:{},{}:] is Relation-like finite set

g is set

O is Relation-like set

O ~ is Relation-like set

A is set

g is set

(O ~) |_2 g is Relation-like set

[:g,g:] is Relation-like set

(O ~) /\ [:g,g:] is Relation-like set

O |_2 g is Relation-like set

O /\ [:g,g:] is Relation-like set

(O |_2 g) ~ is Relation-like set

((O |_2 g) ~) ~ is Relation-like set

AA is set

ff is set

[AA,ff] is V35() set

{AA,ff} is non empty finite set

{AA} is non empty finite set

{{AA,ff},{AA}} is non empty finite V45() set

[ff,AA] is V35() set

{ff,AA} is non empty finite set

{ff} is non empty finite set

{{ff,AA},{ff}} is non empty finite V45() set

g is set

O |_2 g is Relation-like set

[:g,g:] is Relation-like set

O /\ [:g,g:] is Relation-like set

(O ~) |_2 g is Relation-like set

(O ~) /\ [:g,g:] is Relation-like set

(O |_2 g) ~ is Relation-like set

AA is set

ff is set

[ff,AA] is V35() set

{ff,AA} is non empty finite set

{ff} is non empty finite set

{{ff,AA},{ff}} is non empty finite V45() set

[AA,ff] is V35() set

{AA,ff} is non empty finite set

{AA} is non empty finite set

{{AA,ff},{AA}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

(O ~) ~ is Relation-like set

O is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

g is set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

O is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

O is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

O is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

g is set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

O is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

A is set

g is set

AA is set

O |_2 AA is Relation-like set

[:AA,AA:] is Relation-like set

O /\ [:AA,AA:] is Relation-like set

ff is set

[ff,A] is V35() set

{ff,A} is non empty finite set

{ff} is non empty finite set

{{ff,A},{ff}} is non empty finite V45() set

O is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

A is set

g is set

AA is set

O |_2 AA is Relation-like set

[:AA,AA:] is Relation-like set

O /\ [:AA,AA:] is Relation-like set

ff is set

[A,ff] is V35() set

{A,ff} is non empty finite set

{A} is non empty finite set

{{A,ff},{A}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

field (O ~) is set

dom (O ~) is set

rng (O ~) is set

(dom (O ~)) \/ (rng (O ~)) is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

g is set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

field (O ~) is set

dom (O ~) is set

rng (O ~) is set

(dom (O ~)) \/ (rng (O ~)) is set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

g is set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

field (O ~) is set

dom (O ~) is set

rng (O ~) is set

(dom (O ~)) \/ (rng (O ~)) is set

g is set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

O is Relation-like set

O ~ is Relation-like set

A is set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

field (O ~) is set

dom (O ~) is set

rng (O ~) is set

(dom (O ~)) \/ (rng (O ~)) is set

g is set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

g is set

[A,g] is V35() set

{A,g} is non empty finite set

{A} is non empty finite set

{{A,g},{A}} is non empty finite V45() set

[g,A] is V35() set

{g,A} is non empty finite set

{g} is non empty finite set

{{g,A},{g}} is non empty finite V45() set

O is Relation-like set

A is set

g is set

AA is set

O is Relation-like set

field O is set

dom O is set

rng O is set

(dom O) \/ (rng O) is set

A is set

g is non empty set

AA is non empty set

bool AA is non empty Element of bool (bool AA)

bool AA is non empty set

bool (bool AA) is non empty set

(bool AA) \ {{}} is Element of bool (bool AA)

ff is non empty set

union ff is set

the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) is Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff)

z is set

the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . z is set

y is set

AA9 is set

z is set

y is set

the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . z is set

AA9 is set

z is Relation-like Function-like set

dom z is set

y is set

AA9 is set

f9 is epsilon-transitive epsilon-connected ordinal set

x is Relation-like Function-like T-Sequence-like set

rng x is set

{ b

( not b

z . { b

( not b

dom x is epsilon-transitive epsilon-connected ordinal set

x | f9 is Relation-like rng x -valued Function-like T-Sequence-like set

y is Relation-like Function-like T-Sequence-like set

rng y is set

{ b

( not b

z . { b

( not b

dom y is epsilon-transitive epsilon-connected ordinal set

z is epsilon-transitive epsilon-connected ordinal set

x | z is Relation-like rng x -valued Function-like T-Sequence-like set

y | z is Relation-like rng y -valued Function-like T-Sequence-like set

dom (y | z) is epsilon-transitive epsilon-connected ordinal set

a is set

x . a is set

(x | z) . a is set

P2 is epsilon-transitive epsilon-connected ordinal set

x | P2 is Relation-like rng x -valued Function-like T-Sequence-like set

y | P2 is Relation-like rng y -valued Function-like T-Sequence-like set

y . P2 is set

rng (y | P2) is Element of bool (rng y)

bool (rng y) is non empty set

{ b

( not b

z . { b

( not b

x . P2 is set

rng (x | P2) is Element of bool (rng x)

bool (rng x) is non empty set

{ b

( not b

z . { b

( not b

(y | z) . a is set

dom (x | z) is epsilon-transitive epsilon-connected ordinal set

y | f9 is Relation-like rng y -valued Function-like T-Sequence-like set

y is set

z . y is set

the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . y is set

z . {} is set

f9 is Relation-like Function-like T-Sequence-like set

dom f9 is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal set

x is Relation-like Function-like T-Sequence-like set

dom x is epsilon-transitive epsilon-connected ordinal set

AA9 is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal set

z is epsilon-transitive epsilon-connected ordinal set

f9 | z is Relation-like rng f9 -valued Function-like T-Sequence-like set

rng f9 is set

x | z is Relation-like rng x -valued Function-like T-Sequence-like set

rng x is set

dom (x | z) is epsilon-transitive epsilon-connected ordinal set

a is set

f9 . a is set

(f9 | z) . a is set

P2 is epsilon-transitive epsilon-connected ordinal set

f9 | P2 is Relation-like rng f9 -valued Function-like T-Sequence-like set

x | P2 is Relation-like rng x -valued Function-like T-Sequence-like set

x . P2 is set

rng (x | P2) is Element of bool (rng x)

bool (rng x) is non empty set

{ b

( not b

z . { b

( not b

f9 . P2 is set

rng (f9 | P2) is Element of bool (rng f9)

bool (rng f9) is non empty set

{ b

( not b

z . { b

( not b

(x | z) . a is set

dom (f9 | z) is epsilon-transitive epsilon-connected ordinal set

f9 | y is Relation-like rng f9 -valued Function-like T-Sequence-like set

rng f9 is set

x | y is Relation-like rng x -valued Function-like T-Sequence-like set

rng x is set

y is Element of AA

AA9 is epsilon-transitive epsilon-connected ordinal set

f9 is epsilon-transitive epsilon-connected ordinal set

x is Relation-like Function-like T-Sequence-like set

rng x is set

{ b

( not b

z . { b

( not b

dom x is epsilon-transitive epsilon-connected ordinal set

y is Relation-like Function-like T-Sequence-like set

rng y is set

{ b

( not b

z . { b

( not b

dom y is epsilon-transitive epsilon-connected ordinal set

x | f9 is Relation-like rng x -valued Function-like T-Sequence-like set

rng (x | f9) is Element of bool (rng x)

bool (rng x) is non empty set

{ b

( not b

P2 is set

y9 is Element of AA

y | f9 is Relation-like rng y -valued Function-like T-Sequence-like set

x . f9 is set

z . { b

( not b

the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . { b

( not b

P2 is Element of AA

y | AA9 is Relation-like rng y -valued Function-like T-Sequence-like set

rng (y | AA9) is Element of bool (rng y)

bool (rng y) is non empty set

{ b

( not b

P2 is set

y9 is Element of AA

x | AA9 is Relation-like rng x -valued Function-like T-Sequence-like set

y . AA9 is set

z . { b

( not b

the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . { b

( not b

P2 is Element of AA

y is epsilon-transitive epsilon-connected ordinal set

AA9 is set

f9 is epsilon-transitive epsilon-connected ordinal set

x is Element of AA

y is set

z is Relation-like Function-like T-Sequence-like set

rng z is set

{ b

( not b

z . { b

( not b

dom z is epsilon-transitive epsilon-connected ordinal set

AA9 is set

y is epsilon-transitive epsilon-connected ordinal set

f9 is set

z is Relation-like Function-like T-Sequence-like set

rng z is set

{ b

( not b

z . { b

( not b

dom z is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

x is set

P2 is Relation-like Function-like T-Sequence-like set

rng P2 is set

{ b

( not b

z . { b

( not b

dom P2 is epsilon-transitive epsilon-connected ordinal set

AA9 is Relation-like Function-like set

dom AA9 is set

f9 is Relation-like Function-like T-Sequence-like set

rng f9 is set

{ b

( not b

y is set

z is Element of AA

z . { b

( not b

dom f9 is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal set

f9 | y is Relation-like rng f9 -valued Function-like T-Sequence-like set

f9 . y is set

z is Relation-like Function-like T-Sequence-like set

rng z is set

{ b

( not b

z . { b

( not b

a is epsilon-transitive epsilon-connected ordinal set

P2 is Relation-like Function-like T-Sequence-like set

rng P2 is set

{ b

( not b

z . { b

( not b

dom P2 is epsilon-transitive epsilon-connected ordinal set

a is Relation-like Function-like T-Sequence-like set

rng a is set

{ b

( not b

z . { b

( not b

dom a is epsilon-transitive epsilon-connected ordinal set

P2 is set

a . P2 is set

(f9 | y) . P2 is set

f9 . P2 is set

y9 is epsilon-transitive epsilon-connected ordinal set

a | y9 is Relation-like rng a -valued Function-like T-Sequence-like set

z is Relation-like Function-like T-Sequence-like set

rng z is set

{ b

( not b

z . { b

( not b

dom z is epsilon-transitive epsilon-connected ordinal set

z9 is epsilon-transitive epsilon-connected ordinal set

z | z9 is Relation-like rng z -valued Function-like T-Sequence-like set

z . z9 is set

L1 is Relation-like Function-like T-Sequence-like set

rng L1 is set

{ b

( not b

z . { b

( not b

a | z9 is Relation-like rng a -valued Function-like T-Sequence-like set

a . z9 is set

z is epsilon-transitive epsilon-connected ordinal set

z9 is Relation-like Function-like T-Sequence-like set

rng z9 is set

{ b

( not b

z . { b

( not b

dom z9 is epsilon-transitive epsilon-connected ordinal set

L1 is Relation-like Function-like T-Sequence-like set

rng L1 is set

{ b

( not b

z . { b

( not b

dom L1 is epsilon-transitive epsilon-connected ordinal set

dom (f9 | y) is epsilon-transitive epsilon-connected ordinal set

y is Relation-like Function-like T-Sequence-like set

rng y is set

{ b

( not b

z . { b

( not b

dom y is epsilon-transitive epsilon-connected ordinal set

y is Element of AA

z is Relation-like Function-like T-Sequence-like set

rng z is set

{ b

( not b

z . { b

( not b

dom z is epsilon-transitive epsilon-connected ordinal set

y is set

AA9 is set

f9 is set

x is epsilon-transitive epsilon-connected ordinal set

y is Element of AA

z is epsilon-transitive epsilon-connected ordinal set

a is Relation-like Function-like T-Sequence-like set

rng a is set

{ b

( not b

z . { b

( not b

dom a is epsilon-transitive epsilon-connected ordinal set

P2 is Relation-like Function-like T-Sequence-like set

rng P2 is set

{ b

( not b

z . { b

( not b

dom P2 is epsilon-transitive epsilon-connected ordinal set

a is Relation-like Function-like T-Sequence-like set

rng a is set

{ b

( not b

z . { b

( not b

dom a is epsilon-transitive epsilon-connected ordinal set

P2 is Relation-like Function-like T-Sequence-like set

rng P2 is set

{ b

( not b

z . { b

( not b

dom P2 is epsilon-transitive epsilon-connected ordinal set

y is set

AA9 is epsilon-transitive epsilon-connected ordinal set

f9 is Element of AA

x is Relation-like Function-like T-Sequence-like set

rng x is set

{ b

( not b

z . { b

( not b

dom x is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal set

AA9 is Relation-like Function-like T-Sequence-like set

rng AA9 is set

{ b

( not b

f9 is set

x is Element of AA

z . AA is set

AA9 is Element of AA

f9 is Relation-like Function-like T-Sequence-like set

dom f9 is epsilon-transitive epsilon-connected ordinal set

rng f9 is set

{ b

( not b

z . { b

( not b

x is set

y is Element of AA

z is set

[z,y] is V35() set

{z,y} is non empty finite set

{z} is non empty finite set

{{z,y},{z}} is non empty finite V45() set

x is epsilon-transitive epsilon-connected ordinal set

y is Relation-like Function-like T-Sequence-like set

f9 | x is Relation-like rng f9 -valued Function-like T-Sequence-like set

f9 . x is set

rng y is set

{ b

( not b

z . { b

( not b

f9 is set

x is set

x is Relation-like Function-like T-Sequence-like set

rng x is set

{ b

( not b

z . { b

( not b

dom x is epsilon-transitive epsilon-connected ordinal set

y is Relation-like Function-like T-Sequence-like set

rng y is set

{ b

( not b

z . { b

( not b

dom y is epsilon-transitive epsilon-connected ordinal set

y is Relation-like Function-like T-Sequence-like set

rng y is set

{ b

( not b

z . { b

( not b

dom y is epsilon-transitive epsilon-connected ordinal set

y is Relation-like Function-like T-Sequence-like set

rng y is set

{ b

( not b

z . { b

( not b

dom y is epsilon-transitive epsilon-connected ordinal set

y is Relation-like Function-like T-Sequence-like set

rng y is set

{ b

( not b

z . { b

( not b

dom y is epsilon-transitive epsilon-connected ordinal set

x is non empty set

O |_2 x is Relation-like set

[:x,x:] is non empty Relation-like set

O /\ [:x,x:] is Relation-like set

z is set

a is set

y . a is set

P2 is epsilon-transitive epsilon-connected ordinal set

y | P2 is Relation-like rng y -valued Function-like T-Sequence-like set

rng (y | P2) is Element of bool (rng y)

bool (rng y) is non empty set

{ b

( not b

z is Relation-like Function-like T-Sequence-like set

rng z is set

{ b

( not b

z . { b

( not b

dom z is epsilon-transitive epsilon-connected ordinal set

z9 is epsilon-transitive epsilon-connected ordinal set

z | z9 is Relation-like rng z -valued Function-like T-Sequence-like set

z . z9 is set

L1 is Relation-like Function-like T-Sequence-like set

rng L1 is set

{ b

( not b

z . { b

( not b

y | z9 is Relation-like rng y -valued Function-like T-Sequence-like set

y . z9 is set

z is Relation-like Function-like T-Sequence-like set

rng z is set

{ b

( not b

z . { b

( not b

dom z is epsilon-transitive epsilon-connected ordinal set

z9 is Relation-like Function-like T-Sequence-like set

rng z9 is set

{ b

( not b

z . { b

( not b

dom z9 is epsilon-transitive epsilon-connected ordinal set

z . { b

( not b

z is Relation-like Function-like T-Sequence-like set

rng z is set

{ b

( not b

z . { b

( not b

dom z is epsilon-transitive epsilon-connected ordinal set

z is set

field (O |_2 x) is set

dom (O |_2 x) is set

rng (O |_2 x) is set

(dom (O |_2 x)) \/ (rng (O |_2 x)) is set

a is set

[z,a] is V35() set

{z,a} is non empty finite set

{z} is non empty finite set

{{z,a},{z}} is non empty finite V45() set

[a,z] is V35() set

{a,z} is no