:: WELLORD2 semantic presentation

{} is set

the Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty set

field {} is set

X is set

R is Relation-like set

field R is set

dom R is set

rng R is set

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

a is set

b is set

[a,b] is set

{a,b} is set

{a} is set

{{a,b},{a}} is set

b is set

[b,a] is set

{b,a} is set

{b} is set

{{b,a},{b}} is set

a is set

[a,a] is set

{a,a} is set

{a} is set

{{a,a},{a}} is set

a is set

b is set

[a,b] is set

{a,b} is set

{a} is set

{{a,b},{a}} is set

R is Relation-like set

field R is set

dom R is set

rng R is set

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

a is Relation-like set

field a is set

dom a is set

rng a is set

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

b is set

X is set

[b,X] is set

{b,X} is set

{b} is set

{{b,X},{b}} is set

X is set

(X) is Relation-like set

field (X) is set

dom (X) is set

rng (X) is set

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

R is set

[R,R] is set

{R,R} is set

{R} is set

{{R,R},{R}} is set

R is set

field (X) is set

dom (X) is set

rng (X) is set

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

a is set

[R,a] is set

{R,a} is set

{R} is set

{{R,a},{R}} is set

b is set

[a,b] is set

{a,b} is set

{a} is set

{{a,b},{a}} is set

[R,b] is set

{R,b} is set

{{R,b},{R}} is set

field (X) is set

dom (X) is set

rng (X) is set

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

R is set

a is set

[R,a] is set

{R,a} is set

{R} is set

{{R,a},{R}} is set

[a,R] is set

{a,R} is set

{a} is set

{{a,R},{a}} is set

X is epsilon-transitive epsilon-connected ordinal set

(X) is Relation-like reflexive antisymmetric transitive set

R is set

field (X) is set

dom (X) is set

rng (X) is set

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

a is set

[R,a] is set

{R,a} is set

{R} is set

{{R,a},{R}} is set

[a,R] is set

{a,R} is set

{a} is set

{{a,R},{a}} is set

b is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

R is set

field (X) is set

dom (X) is set

rng (X) is set

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

the Element of R is Element of R

b is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

x is set

(X) -Seg x is set

Coim ((X),x) is set

{x} is set

(X) " {x} is set

(Coim ((X),x)) \ {x} is Element of bool (Coim ((X),x))

bool (Coim ((X),x)) is set

((X) -Seg x) /\ R is set

the Element of ((X) -Seg x) /\ R is Element of ((X) -Seg x) /\ R

[ the Element of ((X) -Seg x) /\ R,x] is set

{ the Element of ((X) -Seg x) /\ R,x} is set

{ the Element of ((X) -Seg x) /\ R} is set

{{ the Element of ((X) -Seg x) /\ R,x},{ the Element of ((X) -Seg x) /\ R}} is set

z is epsilon-transitive epsilon-connected ordinal set

X is set

(X) is Relation-like reflexive antisymmetric transitive set

R is set

(R) is Relation-like reflexive antisymmetric transitive set

(R) |_2 X is Relation-like set

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

(R) /\ [:X,X:] is Relation-like set

a is set

b is set

[a,b] is set

{a,b} is set

{a} is set

{{a,b},{a}} is set

field (X) is set

dom (X) is set

rng (X) is set

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

X is epsilon-transitive epsilon-connected ordinal set

R is set

(R) is Relation-like reflexive antisymmetric transitive set

(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

(X) |_2 R is Relation-like set

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

(X) /\ [:R,R:] is Relation-like set

X is epsilon-transitive epsilon-connected ordinal set

R is epsilon-transitive epsilon-connected ordinal set

(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

(R) -Seg X is set

Coim ((R),X) is set

{X} is set

(R) " {X} is set

(Coim ((R),X)) \ {X} is Element of bool (Coim ((R),X))

bool (Coim ((R),X)) is set

a is set

b is epsilon-transitive epsilon-connected ordinal set

[b,X] is set

{b,X} is set

{b} is set

{{b,X},{b}} is set

a is set

[a,X] is set

{a,X} is set

{a} is set

{{a,X},{a}} is set

field (R) is set

dom (R) is set

rng (R) is set

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

b is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

R is epsilon-transitive epsilon-connected ordinal set

(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

field (X) is set

dom (X) is set

rng (X) is set

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

field (R) is set

dom (R) is set

rng (R) is set

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

(R) -Seg X is set

Coim ((R),X) is set

{X} is set

(R) " {X} is set

(Coim ((R),X)) \ {X} is Element of bool (Coim ((R),X))

bool (Coim ((R),X)) is set

(R) |_2 ((R) -Seg X) is Relation-like set

[:((R) -Seg X),((R) -Seg X):] is Relation-like set

(R) /\ [:((R) -Seg X),((R) -Seg X):] is Relation-like set

(X) -Seg R is set

Coim ((X),R) is set

{R} is set

(X) " {R} is set

(Coim ((X),R)) \ {R} is Element of bool (Coim ((X),R))

bool (Coim ((X),R)) is set

(X) |_2 ((X) -Seg R) is Relation-like set

[:((X) -Seg R),((X) -Seg R):] is Relation-like set

(X) /\ [:((X) -Seg R),((X) -Seg R):] is Relation-like set

X is Relation-like set

R is epsilon-transitive epsilon-connected ordinal set

(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

a is epsilon-transitive epsilon-connected ordinal set

(a) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

X is Relation-like set

field X is set

dom X is set

rng X is set

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

R is set

X -Seg R is set

Coim (X,R) is set

{R} is set

X " {R} is set

(Coim (X,R)) \ {R} is Element of bool (Coim (X,R))

bool (Coim (X,R)) is set

X |_2 (X -Seg R) is Relation-like set

[:(X -Seg R),(X -Seg R):] is Relation-like set

X /\ [:(X -Seg R),(X -Seg R):] is Relation-like set

a is epsilon-transitive epsilon-connected ordinal set

(a) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

b is set

X is epsilon-transitive epsilon-connected ordinal set

(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

R is set

X -Seg R is set

Coim (X,R) is set

{R} is set

X " {R} is set

(Coim (X,R)) \ {R} is Element of bool (Coim (X,R))

bool (Coim (X,R)) is set

X |_2 (X -Seg R) is Relation-like set

[:(X -Seg R),(X -Seg R):] is Relation-like set

X /\ [:(X -Seg R),(X -Seg R):] is Relation-like set

a is set

b is set

X is epsilon-transitive epsilon-connected ordinal set

(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

R is Relation-like Function-like set

dom R is set

rng R is set

a is set

b is set

R . b is set

X -Seg b is set

Coim (X,b) is set

{b} is set

X " {b} is set

(Coim (X,b)) \ {b} is Element of bool (Coim (X,b))

bool (Coim (X,b)) is set

X |_2 (X -Seg b) is Relation-like set

[:(X -Seg b),(X -Seg b):] is Relation-like set

X /\ [:(X -Seg b),(X -Seg b):] is Relation-like set

X is epsilon-transitive epsilon-connected ordinal set

(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

a is epsilon-transitive epsilon-connected ordinal set

b is set

X is set

R . X is set

X -Seg X is set

Coim (X,X) is set

{X} is set

X " {X} is set

(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))

bool (Coim (X,X)) is set

X |_2 (X -Seg X) is Relation-like set

[:(X -Seg X),(X -Seg X):] is Relation-like set

X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set

z is epsilon-transitive epsilon-connected ordinal set

(z) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

z is set

[z,b] is set

{z,b} is set

{z} is set

{{z,b},{z}} is set

(a) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

field (a) is set

dom (a) is set

rng (a) is set

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

P is epsilon-transitive epsilon-connected ordinal set

(z) |_2 P is Relation-like set

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

(z) /\ [:P,P:] is Relation-like set

(P) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

(z) -Seg P is set

Coim ((z),P) is set

{P} is set

(z) " {P} is set

(Coim ((z),P)) \ {P} is Element of bool (Coim ((z),P))

bool (Coim ((z),P)) is set

field (z) is set

dom (z) is set

rng (z) is set

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

canonical_isomorphism_of ((z),(X |_2 (X -Seg X))) is Relation-like Function-like set

field (X |_2 (X -Seg X)) is set

dom (X |_2 (X -Seg X)) is set

rng (X |_2 (X -Seg X)) is set

(dom (X |_2 (X -Seg X))) \/ (rng (X |_2 (X -Seg X))) is set

(z) |_2 ((z) -Seg P) is Relation-like set

[:((z) -Seg P),((z) -Seg P):] is Relation-like set

(z) /\ [:((z) -Seg P),((z) -Seg P):] is Relation-like set

d is set

(X |_2 (X -Seg X)) -Seg d is set

Coim ((X |_2 (X -Seg X)),d) is set

{d} is set

(X |_2 (X -Seg X)) " {d} is set

(Coim ((X |_2 (X -Seg X)),d)) \ {d} is Element of bool (Coim ((X |_2 (X -Seg X)),d))

bool (Coim ((X |_2 (X -Seg X)),d)) is set

(X |_2 (X -Seg X)) |_2 ((X |_2 (X -Seg X)) -Seg d) is Relation-like set

[:((X |_2 (X -Seg X)) -Seg d),((X |_2 (X -Seg X)) -Seg d):] is Relation-like set

(X |_2 (X -Seg X)) /\ [:((X |_2 (X -Seg X)) -Seg d),((X |_2 (X -Seg X)) -Seg d):] is Relation-like set

X -Seg d is set

Coim (X,d) is set

X " {d} is set

(Coim (X,d)) \ {d} is Element of bool (Coim (X,d))

bool (Coim (X,d)) is set

[d,X] is set

{d,X} is set

{{d,X},{d}} is set

X |_2 (X -Seg d) is Relation-like set

[:(X -Seg d),(X -Seg d):] is Relation-like set

X /\ [:(X -Seg d),(X -Seg d):] is Relation-like set

R . d is set

b is set

(a) -Seg b is set

Coim ((a),b) is set

{b} is set

(a) " {b} is set

(Coim ((a),b)) \ {b} is Element of bool (Coim ((a),b))

bool (Coim ((a),b)) is set

b is epsilon-transitive epsilon-connected ordinal set

(b) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

field (b) is set

dom (b) is set

rng (b) is set

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

X is set

R . X is set

X is set

R . X is set

x is set

R . x is set

X -Seg x is set

Coim (X,x) is set

{x} is set

X " {x} is set

(Coim (X,x)) \ {x} is Element of bool (Coim (X,x))

bool (Coim (X,x)) is set

X |_2 (X -Seg x) is Relation-like set

[:(X -Seg x),(X -Seg x):] is Relation-like set

X /\ [:(X -Seg x),(X -Seg x):] is Relation-like set

y is epsilon-transitive epsilon-connected ordinal set

(y) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

X -Seg X is set

Coim (X,X) is set

{X} is set

X " {X} is set

(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))

bool (Coim (X,X)) is set

X |_2 (X -Seg X) is Relation-like set

[:(X -Seg X),(X -Seg X):] is Relation-like set

X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set

X is set

R . X is set

x is set

[X,x] is set

{X,x} is set

{X} is set

{{X,x},{X}} is set

R . x is set

[(R . X),(R . x)] is set

{(R . X),(R . x)} is set

{(R . X)} is set

{{(R . X),(R . x)},{(R . X)}} is set

X -Seg x is set

Coim (X,x) is set

{x} is set

X " {x} is set

(Coim (X,x)) \ {x} is Element of bool (Coim (X,x))

bool (Coim (X,x)) is set

X |_2 (X -Seg x) is Relation-like set

[:(X -Seg x),(X -Seg x):] is Relation-like set

X /\ [:(X -Seg x),(X -Seg x):] is Relation-like set

P is epsilon-transitive epsilon-connected ordinal set

(P) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

z is epsilon-transitive epsilon-connected ordinal set

X -Seg X is set

Coim (X,X) is set

X " {X} is set

(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))

bool (Coim (X,X)) is set

X |_2 (X -Seg X) is Relation-like set

[:(X -Seg X),(X -Seg X):] is Relation-like set

X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set

(z) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

(X |_2 (X -Seg x)) -Seg X is set

Coim ((X |_2 (X -Seg x)),X) is set

(X |_2 (X -Seg x)) " {X} is set

(Coim ((X |_2 (X -Seg x)),X)) \ {X} is Element of bool (Coim ((X |_2 (X -Seg x)),X))

bool (Coim ((X |_2 (X -Seg x)),X)) is set

field (X |_2 (X -Seg x)) is set

dom (X |_2 (X -Seg x)) is set

rng (X |_2 (X -Seg x)) is set

(dom (X |_2 (X -Seg x))) \/ (rng (X |_2 (X -Seg x))) is set

(b) |_2 z is Relation-like set

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

(b) /\ [:z,z:] is Relation-like set

(b) -Seg z is set

Coim ((b),z) is set

{z} is set

(b) " {z} is set

(Coim ((b),z)) \ {z} is Element of bool (Coim ((b),z))

bool (Coim ((b),z)) is set

(X |_2 (X -Seg x)) |_2 ((X |_2 (X -Seg x)) -Seg X) is Relation-like set

[:((X |_2 (X -Seg x)) -Seg X),((X |_2 (X -Seg x)) -Seg X):] is Relation-like set

(X |_2 (X -Seg x)) /\ [:((X |_2 (X -Seg x)) -Seg X),((X |_2 (X -Seg x)) -Seg X):] is Relation-like set

(b) |_2 ((b) -Seg z) is Relation-like set

[:((b) -Seg z),((b) -Seg z):] is Relation-like set

(b) /\ [:((b) -Seg z),((b) -Seg z):] is Relation-like set

(b) -Seg P is set

Coim ((b),P) is set

{P} is set

(b) " {P} is set

(Coim ((b),P)) \ {P} is Element of bool (Coim ((b),P))

bool (Coim ((b),P)) is set

(b) |_2 ((b) -Seg P) is Relation-like set

[:((b) -Seg P),((b) -Seg P):] is Relation-like set

(b) /\ [:((b) -Seg P),((b) -Seg P):] is Relation-like set

[z,P] is set

{z,P} is set

{{z,P},{z}} is set

[x,X] is set

{x,X} is set

{x} is set

{{x,X},{x}} is set

X -Seg x is set

Coim (X,x) is set

X " {x} is set

(Coim (X,x)) \ {x} is Element of bool (Coim (X,x))

bool (Coim (X,x)) is set

X -Seg X is set

Coim (X,X) is set

X " {X} is set

(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))

bool (Coim (X,X)) is set

X |_2 (X -Seg X) is Relation-like set

[:(X -Seg X),(X -Seg X):] is Relation-like set

X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set

y is epsilon-transitive epsilon-connected ordinal set

(y) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

X |_2 (X -Seg x) is Relation-like set

[:(X -Seg x),(X -Seg x):] is Relation-like set

X /\ [:(X -Seg x),(X -Seg x):] is Relation-like set

z is epsilon-transitive epsilon-connected ordinal set

(z) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

(b) |_2 z is Relation-like set

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

(b) /\ [:z,z:] is Relation-like set

(b) -Seg y is set

Coim ((b),y) is set

{y} is set

(b) " {y} is set

(Coim ((b),y)) \ {y} is Element of bool (Coim ((b),y))

bool (Coim ((b),y)) is set

(b) |_2 ((b) -Seg y) is Relation-like set

[:((b) -Seg y),((b) -Seg y):] is Relation-like set

(b) /\ [:((b) -Seg y),((b) -Seg y):] is Relation-like set

(X |_2 (X -Seg X)) -Seg x is set

Coim ((X |_2 (X -Seg X)),x) is set

(X |_2 (X -Seg X)) " {x} is set

(Coim ((X |_2 (X -Seg X)),x)) \ {x} is Element of bool (Coim ((X |_2 (X -Seg X)),x))

bool (Coim ((X |_2 (X -Seg X)),x)) is set

(b) -Seg z is set

Coim ((b),z) is set

{z} is set

(b) " {z} is set

(Coim ((b),z)) \ {z} is Element of bool (Coim ((b),z))

bool (Coim ((b),z)) is set

(X |_2 (X -Seg X)) |_2 ((X |_2 (X -Seg X)) -Seg x) is Relation-like set

[:((X |_2 (X -Seg X)) -Seg x),((X |_2 (X -Seg X)) -Seg x):] is Relation-like set

(X |_2 (X -Seg X)) /\ [:((X |_2 (X -Seg X)) -Seg x),((X |_2 (X -Seg X)) -Seg x):] is Relation-like set

(b) |_2 ((b) -Seg z) is Relation-like set

[:((b) -Seg z),((b) -Seg z):] is Relation-like set

(b) /\ [:((b) -Seg z),((b) -Seg z):] is Relation-like set

field (X |_2 (X -Seg X)) is set

dom (X |_2 (X -Seg X)) is set

rng (X |_2 (X -Seg X)) is set

(dom (X |_2 (X -Seg X))) \/ (rng (X |_2 (X -Seg X))) is set

[z,y] is set

{z,y} is set

{{z,y},{z}} is set

X is Relation-like set

field X is set

dom X is set

rng X is set

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

R is set

a is set

X -Seg a is set

Coim (X,a) is set

{a} is set

X " {a} is set

(Coim (X,a)) \ {a} is Element of bool (Coim (X,a))

bool (Coim (X,a)) is set

X |_2 (X -Seg a) is Relation-like set

[:(X -Seg a),(X -Seg a):] is Relation-like set

X /\ [:(X -Seg a),(X -Seg a):] is Relation-like set

X is set

field (X |_2 (X -Seg a)) is set

dom (X |_2 (X -Seg a)) is set

rng (X |_2 (X -Seg a)) is set

(dom (X |_2 (X -Seg a))) \/ (rng (X |_2 (X -Seg a))) is set

[X,a] is set

{X,a} is set

{X} is set

{{X,a},{X}} is set

X -Seg X is set

Coim (X,X) is set

X " {X} is set

(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))

bool (Coim (X,X)) is set

X |_2 (X -Seg X) is Relation-like set

[:(X -Seg X),(X -Seg X):] is Relation-like set

X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set

x is epsilon-transitive epsilon-connected ordinal set

(x) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

(X |_2 (X -Seg a)) -Seg X is set

Coim ((X |_2 (X -Seg a)),X) is set

(X |_2 (X -Seg a)) " {X} is set

(Coim ((X |_2 (X -Seg a)),X)) \ {X} is Element of bool (Coim ((X |_2 (X -Seg a)),X))

bool (Coim ((X |_2 (X -Seg a)),X)) is set

(X |_2 (X -Seg a)) |_2 ((X |_2 (X -Seg a)) -Seg X) is Relation-like set

[:((X |_2 (X -Seg a)) -Seg X),((X |_2 (X -Seg a)) -Seg X):] is Relation-like set

(X |_2 (X -Seg a)) /\ [:((X |_2 (X -Seg a)) -Seg X),((X |_2 (X -Seg a)) -Seg X):] is Relation-like set

y is epsilon-transitive epsilon-connected ordinal set

(y) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

X is epsilon-transitive epsilon-connected ordinal set

(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

a is set

X -Seg a is set

Coim (X,a) is set

{a} is set

X " {a} is set

(Coim (X,a)) \ {a} is Element of bool (Coim (X,a))

bool (Coim (X,a)) is set

X |_2 (X -Seg a) is Relation-like set

[:(X -Seg a),(X -Seg a):] is Relation-like set

X /\ [:(X -Seg a),(X -Seg a):] is Relation-like set

X is Relation-like set

R is epsilon-transitive epsilon-connected ordinal set

(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

a is epsilon-transitive epsilon-connected ordinal set

(a) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

X is set

(X) is Relation-like reflexive antisymmetric transitive set

((X)) is epsilon-transitive epsilon-connected ordinal set

R is epsilon-transitive epsilon-connected ordinal set

(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

(R) |_2 X is Relation-like set

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

(R) /\ [:X,X:] is Relation-like set

a is set

(R) -Seg a is set

Coim ((R),a) is set

{a} is set

(R) " {a} is set

(Coim ((R),a)) \ {a} is Element of bool (Coim ((R),a))

bool (Coim ((R),a)) is set

(R) |_2 ((R) -Seg a) is Relation-like set

[:((R) -Seg a),((R) -Seg a):] is Relation-like set

(R) /\ [:((R) -Seg a),((R) -Seg a):] is Relation-like set

b is epsilon-transitive epsilon-connected ordinal set

(R) -Seg b is set

Coim ((R),b) is set

{b} is set

(R) " {b} is set

(Coim ((R),b)) \ {b} is Element of bool (Coim ((R),b))

bool (Coim ((R),b)) is set

(R) |_2 b is Relation-like set

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

(R) /\ [:b,b:] is Relation-like set

(b) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

field (R) is set

dom (R) is set

rng (R) is set

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

X is set

R is set

a is set

[:X,R:] is Relation-like set

a /\ [:X,R:] is Relation-like set

X is set

x is set

[X,x] is set

{X,x} is set

{X} is set

{{X,x},{X}} is set

y is set

[X,y] is set

{X,y} is set

{{X,y},{X}} is set

X is Relation-like Function-like set

x is Relation-like Function-like set

dom x is set

rng x is set

y is set

x . y is set

z is set

x . z is set

[z,(x . z)] is set

{z,(x . z)} is set

{z} is set

{{z,(x . z)},{z}} is set

[y,(x . y)] is set

{y,(x . y)} is set

{y} is set

{{y,(x . y)},{y}} is set

y is set

x . y is set

[y,(x . y)] is set

{y,(x . y)} is set

{y} is set

{{y,(x . y)},{y}} is set

y is set

z is set

[y,z] is set

{y,z} is set

{y} is set

{{y,z},{y}} is set

y is set

z is set

x . z is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

y is set

z is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

x . z is set

a is Relation-like Function-like set

dom a is set

rng a is set

b is Relation-like Function-like set

X is set

a . X is set

[X,(a . X)] is set

{X,(a . X)} is set

{X} is set

{{X,(a . X)},{X}} is set

X is set

a " is Relation-like Function-like set

(a ") . X is set

[((a ") . X),X] is set

{((a ") . X),X} is set

{((a ") . X)} is set

{{((a ") . X),X},{((a ") . X)}} is set

dom (a ") is set

rng (a ") is set

a . ((a ") . X) is set

X is set

x is set

[X,x] is set

{X,x} is set

{X} is set

{{X,x},{X}} is set

y is set

z is set

[y,z] is set

{y,z} is set

{y} is set

{{y,z},{y}} is set

a . X is set

a . y is set

a is Relation-like Function-like set

dom a is set

rng a is set

b is set

a is set

id a is Relation-like a -defined a -valued Function-like one-to-one set

dom (id a) is set

rng (id a) is set

a is set

b is set

X is Relation-like Function-like set

dom X is set

rng X is set

X " is Relation-like Function-like set

dom (X ") is set

rng (X ") is set

X is set

R is set

a is set

b is Relation-like Function-like set

dom b is set

rng b is set

X is Relation-like Function-like set

dom X is set

rng X is set

b * X is Relation-like Function-like set

dom (b * X) is set

rng (b * X) is set

X is set

R is Relation-like set

R |_2 X is Relation-like set

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

R /\ [:X,X:] is Relation-like set

field (R |_2 X) is set

dom (R |_2 X) is set

rng (R |_2 X) is set

(dom (R |_2 X)) \/ (rng (R |_2 X)) is set

a is set

b is set

[a,b] is set

{a,b} is set

{a} is set

{{a,b},{a}} is set

[b,a] is set

{b,a} is set

{b} is set

{{b,a},{b}} is set

a is set

b is set

R -Seg b is set

Coim (R,b) is set

{b} is set

R " {b} is set

(Coim (R,b)) \ {b} is Element of bool (Coim (R,b))

bool (Coim (R,b)) is set

(R |_2 X) -Seg b is set

Coim ((R |_2 X),b) is set

(R |_2 X) " {b} is set

(Coim ((R |_2 X),b)) \ {b} is Element of bool (Coim ((R |_2 X),b))

bool (Coim ((R |_2 X),b)) is set

X is set

[X,b] is set

{X,b} is set

{X} is set

{{X,b},{X}} is set

a is set

b is set

[a,b] is set

{a,b} is set

{a} is set

{{a,b},{a}} is set

X is set

[b,X] is set

{b,X} is set

{b} is set

{{b,X},{b}} is set

[a,X] is set

{a,X} is set

{{a,X},{a}} is set

a is set

b is set

[a,b] is set

{a,b} is set

{a} is set

{{a,b},{a}} is set

[b,a] is set

{b,a} is set

{b} is set

{{b,a},{b}} is set

a is set

[a,a] is set

{a,a} is set

{a} is set

{{a,a},{a}} is set

a is set

[a,a] is set

{a,a} is set

{a} is set

{{a,a},{a}} is set

X is set

R is Relation-like set

field R is set

dom R is set

rng R is set

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

a is Relation-like Function-like set

dom a is set

rng a is set

b is Relation-like set

field b is set

dom b is set

rng b is set

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

X is set

x is set

[x,X] is set

{x,X} is set

{x} is set

{{x,X},{x}} is set

x is set

[X,x] is set

{X,x} is set

{X} is set

{{X,x},{X}} is set

X is set

a . X is set

[(a . X),(a . X)] is set

{(a . X),(a . X)} is set

{(a . X)} is set

{{(a . X),(a . X)},{(a . X)}} is set

[X,X] is set

{X,X} is set

{X} is set

{{X,X},{X}} is set

X is set

a . X is set

x is set

[X,x] is set

{X,x} is set

{X} is set

{{X,x},{X}} is set

a . x is set

[(a . X),(a . x)] is set

{(a . X),(a . x)} is set

{(a . X)} is set

{{(a . X),(a . x)},{(a . X)}} is set

a " is Relation-like Function-like set

X is set

R is set

a is set

b is set

x is set

X is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

X is set

(b) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set

field (b) is set

dom (b) is set

rng (b) is set

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

X is Relation-like set

x is Relation-like Function-like set

dom x is set

rng x is set

y is set

z is set

x . z is set

{z} is set

z is set

y is set

x . y is set

z is set

x . z is set

{y} is set

{z} is set

X |_2 R is Relation-like set

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

X /\ [:R,R:] is Relation-like set

field (X |_2 R) is set

dom (X |_2 R) is set

rng (X |_2 R) is set

(dom (X |_2 R)) \/ (rng (X |_2 R)) is set

(X |_2 R) |_2 (rng x) is Relation-like set

[:(rng x),(rng x):] is Relation-like set

(X |_2 R) /\ [:(rng x),(rng x):] is Relation-like set

field ((X |_2 R) |_2 (rng x)) is set

dom ((X |_2 R) |_2 (rng x)) is set

rng ((X |_2 R) |_2 (rng x)) is set

(dom ((X |_2 R) |_2 (rng x))) \/ (rng ((X |_2 R) |_2 (rng x))) is set

X is non empty set

union X is set

R is Relation-like set

a is set

b is set

X is set

[b,X] is set

{b,X} is set

{b} is set

{{b,X},{b}} is set

[X,b] is set

{X,b} is set

{X} is set

{{X,b},{X}} is set

a is set

b is set

R -Seg b is set

Coim (R,b) is set

{b} is set

R " {b} is set

(Coim (R,b)) \ {b} is Element of bool (Coim (R,b))

bool (Coim (R,b)) is set

X is set

[b,X] is set

{b,X} is set

{{b,X},{b}} is set

[X,b] is set

{X,b} is set

{X} is set

{{X,b},{X}} is set

a is Relation-like Function-like set

dom a is set

rng a is set

b is set

X is set

b /\ X is set

a . X is set

x is set

{x} is set

y is set

z is set

a . z is set

X /\ z is set

y is set

X is set

(X) is Relation-like reflexive antisymmetric transitive set

field (X) is set

dom (X) is set

rng (X) is set

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

X is set

(X) is Relation-like reflexive antisymmetric transitive set

field (X) is set

dom (X) is set

rng (X) is set

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

X is set

(X) is Relation-like reflexive antisymmetric transitive set

field (X) is set

dom (X) is set

rng (X) is set

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

({}) is Relation-like reflexive antisymmetric transitive set

X is set

R is set

[X,R] is set

{X,R} is set

{X} is set

{{X,R},{X}} is set

X is non empty set

(X) is Relation-like reflexive antisymmetric transitive set

the Element of X is Element of X

[ the Element of X, the Element of X] is set

{ the Element of X, the Element of X} is set

{ the Element of X} is set

{{ the Element of X, the Element of X},{ the Element of X}} is set

X is set

{X} is set

({X}) is Relation-like reflexive antisymmetric transitive set

[X,X] is set

{X,X} is set

{{X,X},{X}} is set

{[X,X]} is Relation-like Function-like set

R is set

a is set

[R,a] is set

{R,a} is set

{R} is set

{{R,a},{R}} is set

field {[X,X]} is set

dom {[X,X]} is set

rng {[X,X]} is set

(dom {[X,X]}) \/ (rng {[X,X]}) is set

X is set

(X) is Relation-like reflexive antisymmetric transitive set

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

a is set

b is set

[a,b] is set

{a,b} is set

{a} is set

{{a,b},{a}} is set

field (X) is set

dom (X) is set

rng (X) is set

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