:: ORDERS_1 semantic presentation

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,():] is Relation-like set
bool [:O,():] is non empty set
the Element of O is Element of O

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

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

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

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

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

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

[:AA,(union AA):] is Relation-like set
bool [:AA,(union AA):] is non empty set
[:(union AA),():] is Relation-like set
bool [:(union AA),():] 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),():]
y * (x * AA9) is Relation-like O -defined union O -valued Function-like Element of bool [:O,():]

a is set
z . a is set
AA9 . a is set
{a} is non empty finite 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

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

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

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

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

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

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

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

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

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

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

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

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 set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set

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

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

field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
[:(),():] 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

field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is 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

A is set

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

A is set

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

A is set

[:A,A:] is Relation-like set
O /\ [:A,A:] 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

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

A is set

A is set

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

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

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

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

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

A is set

[:A,A:] is Relation-like set
O /\ [:A,A:] 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

A is set

[:A,A:] is Relation-like set
O /\ [:A,A:] 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

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

A is set
g is set

A is set

[:A,A:] is Relation-like set
O /\ [:A,A:] 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

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

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

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

A is set

A is set

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

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

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

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

A is set

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

A is set

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

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

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

A is set

g is set

A is set

g is 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 /\ [: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

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

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

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

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

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

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

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

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

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

A is set
g is set
AA is 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

dom z is set
y is set
AA9 is set

rng x is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng y is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

a is set
x . a is set
(x | z) . a is set

y . P2 is set
rng (y | P2) is Element of bool (rng y)
bool (rng y) is non empty set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (y | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (y | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

x . P2 is set
rng (x | P2) is Element of bool (rng x)
bool (rng x) is non empty set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (x | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (x | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

(y | z) . a is 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

rng f9 is set

rng x is set

a is set
f9 . a is set
(f9 | z) . a is set

x . P2 is set
rng (x | P2) is Element of bool (rng x)
bool (rng x) is non empty set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (x | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (x | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

f9 . P2 is set
rng (f9 | P2) is Element of bool (rng f9)
bool (rng f9) is non empty set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (f9 | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (f9 | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

(x | z) . a is set

rng f9 is set

rng x is set
y is Element of AA

rng x is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng y is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng (x | f9) is Element of bool (rng x)
bool (rng x) is non empty set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (x | f9) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

P2 is set
y9 is Element of AA

x . f9 is set
z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (x | f9) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

P2 is Element of AA

rng (y | AA9) is Element of bool (rng y)
bool (rng y) is non empty set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (y | AA9) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

P2 is set
y9 is Element of AA

y . AA9 is set
z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (y | AA9) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

P2 is Element of AA

AA9 is set

x is Element of AA
y is set

rng z is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

AA9 is set

f9 is set

rng z is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

x is set

rng P2 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng P2 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng P2 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

dom AA9 is set

rng f9 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng f9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

y is set
z is Element of AA
z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng f9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

f9 . y is set

rng z is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng P2 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng P2 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng P2 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng a is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng a or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng a or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

P2 is set
a . P2 is set
(f9 | y) . P2 is set
f9 . P2 is set

rng z is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . z9 is set

rng L1 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng L1 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng L1 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

a . z9 is set

rng z9 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng L1 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng L1 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng L1 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng y is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

y is Element of AA

rng z is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

y is set
AA9 is set
f9 is set

y is Element of AA

rng a is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng a or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng a or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng P2 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng P2 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng P2 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng a is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng a or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng a or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng P2 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng P2 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng P2 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

y is set

f9 is Element of AA

rng x is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng AA9 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng AA9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

f9 is set
x is Element of AA
z . AA is set
AA9 is Element of AA

rng f9 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng f9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng f9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

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

f9 . x is set
rng y is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

f9 is set
x is set

rng x is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng x or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng y is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng y is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng y is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng y is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng y or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

x is non empty 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

rng (y | P2) is Element of bool (rng y)
bool (rng y) is non empty set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (y | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng z is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . z9 is set

rng L1 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng L1 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng L1 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

y . z9 is set

rng z is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng z9 is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z9 or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng (y | P2) or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

rng z is set
{ b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is set

z . { b1 where b1 is Element of AA : for b2 being set holds
( not b2 in rng z or ( not b2 = b1 & [b2,b1] in O ) )
}
is 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