:: YELLOW_1 semantic presentation

K218() is set

K222() is non empty V12() V13() V14() V42() V47() V48() Element of bool K218()

bool K218() is non empty set

K46() is non empty V12() V13() V14() V42() V47() V48() set

bool K46() is non empty V42() set

bool K222() is non empty V42() set

K267() is set

{} is empty V12() V13() V14() V16() V17() V18() V42() V47() V49( {} ) set

the empty V12() V13() V14() V16() V17() V18() V42() V47() V49( {} ) set is empty V12() V13() V14() V16() V17() V18() V42() V47() V49( {} ) set

{{}} is non empty trivial V49(1) set

1 is non empty V12() V13() V14() V18() V42() V47() Element of K222()

K245({{}}) is M18({{}})

[:K245({{}}),{{}}:] is set

bool [:K245({{}}),{{}}:] is non empty set

K58(K245({{}}),{{}}) is non empty functional set

{{},1} is non empty set

product {} is set

S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

LattPOSet S is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of S is non empty set

K167(S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S,K167(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr

LattPOSet S is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of S is non empty set

K167(S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S,K167(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (LattPOSet S) is non empty set

Top (LattPOSet S) is Element of the carrier of (LattPOSet S)

T is Element of the carrier of (LattPOSet S)

A1 is Element of the carrier of S

Top S is Element of the carrier of S

a is Element of the carrier of (LattPOSet S)

f is Element of the carrier of S

f % is Element of the carrier of (LattPOSet S)

A1 % is Element of the carrier of (LattPOSet S)

A2 is Element of the carrier of (LattPOSet S)

"/\" ({},(LattPOSet S)) is Element of the carrier of (LattPOSet S)

f is Element of the carrier of (LattPOSet S)

x9 is Element of the carrier of S

a is Element of the carrier of S

x9 % is Element of the carrier of (LattPOSet S)

a % is Element of the carrier of (LattPOSet S)

T is Element of the carrier of (LattPOSet S)

S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr

LattPOSet S is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of S is non empty set

K167(S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S,K167(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (LattPOSet S) is non empty set

Bottom (LattPOSet S) is Element of the carrier of (LattPOSet S)

T is Element of the carrier of (LattPOSet S)

A1 is Element of the carrier of S

Bottom S is Element of the carrier of S

a is Element of the carrier of (LattPOSet S)

f is Element of the carrier of S

f % is Element of the carrier of (LattPOSet S)

A1 % is Element of the carrier of (LattPOSet S)

A2 is Element of the carrier of (LattPOSet S)

"\/" ({},(LattPOSet S)) is Element of the carrier of (LattPOSet S)

f is Element of the carrier of (LattPOSet S)

a is Element of the carrier of S

x9 is Element of the carrier of S

x9 % is Element of the carrier of (LattPOSet S)

a % is Element of the carrier of (LattPOSet S)

T is Element of the carrier of (LattPOSet S)

S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr

LattPOSet S is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of S is non empty set

K167(S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S,K167(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (LattPOSet S) is non empty set

T is set

"\/" (T,(LattPOSet S)) is Element of the carrier of (LattPOSet S)

A1 is Element of the carrier of (LattPOSet S)

"\/" (T,S) is Element of the carrier of S

("\/" (T,S)) % is Element of the carrier of (LattPOSet S)

A2 is Element of the carrier of (LattPOSet S)

a is Element of the carrier of S

a % is Element of the carrier of (LattPOSet S)

S is set

RelIncl S is Relation-like reflexive antisymmetric transitive set

[:S,S:] is set

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

T is set

A1 is set

A2 is set

[A1,A2] is set

{A1,A2} is non empty set

{A1} is non empty trivial V49(1) set

{{A1,A2},{A1}} is non empty set

field (RelIncl S) is set

dom (RelIncl S) is set

rng (RelIncl S) is set

(dom (RelIncl S)) \/ (rng (RelIncl S)) is set

T is Relation-like S -defined S -valued Element of bool [:S,S:]

field T is set

dom T is set

rng T is set

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

dom T is Element of bool S

bool S is non empty set

S is set

(S) is Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is set

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

RelStr(# S,(S) #) is strict V84() reflexive transitive antisymmetric RelStr

S is set

(S) is strict RelStr

(S) is Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is set

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

RelStr(# S,(S) #) is strict V84() reflexive transitive antisymmetric RelStr

S is non empty set

(S) is strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

S is set

(S) is strict V84() reflexive transitive antisymmetric RelStr

(S) is Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is set

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

RelStr(# S,(S) #) is strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is set

T is set

(T) is strict V84() reflexive transitive antisymmetric RelStr

(T) is Relation-like T -defined T -valued reflexive antisymmetric transitive V34(T) Element of bool [:T,T:]

[:T,T:] is set

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

RelStr(# T,(T) #) is strict V84() reflexive transitive antisymmetric RelStr

the InternalRel of (T) is Relation-like the carrier of (T) -defined the carrier of (T) -valued reflexive antisymmetric transitive V34( the carrier of (T)) Element of bool [: the carrier of (T), the carrier of (T):]

the carrier of (T) is set

[: the carrier of (T), the carrier of (T):] is set

bool [: the carrier of (T), the carrier of (T):] is non empty set

S is set

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

S is set

(S) is strict RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is Element of the carrier of (S)

A2 is Element of the carrier of (BooleLatt S)

A2 % is Element of the carrier of (LattPOSet (BooleLatt S))

the carrier of (LattPOSet (BooleLatt S)) is non empty set

a is Element of the carrier of (BooleLatt S)

a % is Element of the carrier of (LattPOSet (BooleLatt S))

A2 is Element of the carrier of (BooleLatt S)

a is Element of the carrier of (BooleLatt S)

A2 % is Element of the carrier of (LattPOSet (BooleLatt S))

the carrier of (LattPOSet (BooleLatt S)) is non empty set

a % is Element of the carrier of (LattPOSet (BooleLatt S))

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is Element of the carrier of (S)

[T,A1] is set

{T,A1} is non empty set

{T} is non empty trivial V49(1) set

{{T,A1},{T}} is non empty set

the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued reflexive antisymmetric transitive V34( the carrier of (S)) Element of bool [: the carrier of (S), the carrier of (S):]

[: the carrier of (S), the carrier of (S):] is non empty set

bool [: the carrier of (S), the carrier of (S):] is non empty set

[T,A1] is set

{T,A1} is non empty set

{T} is non empty trivial V49(1) set

{{T,A1},{T}} is non empty set

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

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

bool S is non empty set

bool (bool S) is non empty set

((bool S)) is non empty strict V84() reflexive transitive antisymmetric RelStr

((bool S)) is non empty Relation-like bool S -defined bool S -valued reflexive antisymmetric transitive V34( bool S) Element of bool [:(bool S),(bool S):]

[:(bool S),(bool S):] is non empty set

bool [:(bool S),(bool S):] is non empty set

RelStr(# (bool S),((bool S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued reflexive antisymmetric transitive V34( the carrier of (S)) Element of bool [: the carrier of (S), the carrier of (S):]

[: the carrier of (S), the carrier of (S):] is non empty set

bool [: the carrier of (S), the carrier of (S):] is non empty set

A1 is Relation-like bool S -defined bool S -valued Element of bool [:(bool S),(bool S):]

A2 is set

a is Element of the carrier of (S)

f is Element of the carrier of (S)

[A2,f] is set

{A2,f} is non empty set

{A2} is non empty trivial V49(1) set

{{A2,f},{A2}} is non empty set

dom A1 is Element of bool (bool S)

bool (bool S) is non empty set

A2 is set

a is set

[A2,a] is set

{A2,a} is non empty set

{A2} is non empty trivial V49(1) set

{{A2,a},{A2}} is non empty set

f is Element of the carrier of (S)

x9 is Element of the carrier of (S)

f is Element of the carrier of (S)

x9 is Element of the carrier of (S)

A2 is set

a is Element of the carrier of (S)

f is Element of the carrier of (S)

[f,A2] is set

{f,A2} is non empty set

{f} is non empty trivial V49(1) set

{{f,A2},{f}} is non empty set

field the InternalRel of (S) is set

dom the InternalRel of (S) is set

rng the InternalRel of (S) is set

(dom the InternalRel of (S)) \/ (rng the InternalRel of (S)) is set

(bool S) \/ (bool S) is non empty Element of bool (bool S)

S is set

bool S is non empty set

bool (bool S) is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

A1 is Element of bool (bool S)

(A1) is strict V84() reflexive transitive antisymmetric RelStr

(A1) is Relation-like A1 -defined A1 -valued reflexive antisymmetric transitive V34(A1) Element of bool [:A1,A1:]

[:A1,A1:] is set

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

RelStr(# A1,(A1) #) is strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

bool the carrier of (S) is non empty set

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

[:(bool S),(bool S):] is non empty set

bool [:(bool S),(bool S):] is non empty set

the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued reflexive antisymmetric transitive V34( the carrier of (S)) Element of bool [: the carrier of (S), the carrier of (S):]

[: the carrier of (S), the carrier of (S):] is non empty set

bool [: the carrier of (S), the carrier of (S):] is non empty set

a is Relation-like bool S -defined bool S -valued Element of bool [:(bool S),(bool S):]

f is set

x9 is Element of the carrier of (S)

f is Element of the carrier of (S)

[f,f] is set

{f,f} is non empty set

{f} is non empty trivial V49(1) set

{{f,f},{f}} is non empty set

dom a is Element of bool (bool S)

bool (bool S) is non empty set

f is set

x9 is set

[f,x9] is set

{f,x9} is non empty set

{f} is non empty trivial V49(1) set

{{f,x9},{f}} is non empty set

f is Element of the carrier of (S)

z is Element of the carrier of (S)

f is Element of the carrier of (S)

z is Element of the carrier of (S)

f is set

x9 is Element of the carrier of (S)

f is Element of the carrier of (S)

[f,f] is set

{f,f} is non empty set

{f} is non empty trivial V49(1) set

{{f,f},{f}} is non empty set

field the InternalRel of (S) is set

dom the InternalRel of (S) is set

rng the InternalRel of (S) is set

(dom the InternalRel of (S)) \/ (rng the InternalRel of (S)) is set

(bool S) \/ (bool S) is non empty Element of bool (bool S)

((bool S)) is non empty Relation-like bool S -defined bool S -valued reflexive antisymmetric transitive V34( bool S) Element of bool [:(bool S),(bool S):]

A2 is Element of bool the carrier of (S)

the InternalRel of (S) |_2 A2 is Relation-like A2 -defined A2 -valued Element of bool [:A2,A2:]

[:A2,A2:] is set

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

RelStr(# A2,( the InternalRel of (S) |_2 A2) #) is strict RelStr

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is Element of the carrier of (S)

T \/ A1 is set

T "\/" A1 is Element of the carrier of (S)

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is Element of the carrier of (S)

T "/\" A1 is Element of the carrier of (S)

T /\ A1 is set

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is Element of the carrier of (S)

T \/ A1 is set

T "\/" A1 is Element of the carrier of (S)

A2 is Element of the carrier of (S)

a is Element of the carrier of (S)

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is Element of the carrier of (S)

T /\ A1 is set

T "/\" A1 is Element of the carrier of (S)

A2 is Element of the carrier of (S)

a is Element of the carrier of (S)

S is RelStr

the carrier of S is set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is set

bool [: the carrier of S, the carrier of S:] is non empty set

( the carrier of S) is Relation-like the carrier of S -defined the carrier of S -valued reflexive antisymmetric transitive V34( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]

T is set

A1 is set

[T,A1] is set

{T,A1} is non empty set

{T} is non empty trivial V49(1) set

{{T,A1},{T}} is non empty set

A2 is Element of the carrier of S

a is Element of the carrier of S

A2 is Element of the carrier of S

a is Element of the carrier of S

T is set

A1 is Element of the carrier of S

A2 is Element of the carrier of S

[T,A2] is set

{T,A2} is non empty set

{T} is non empty trivial V49(1) set

{{T,A2},{T}} is non empty set

dom the InternalRel of S is Element of bool the carrier of S

bool the carrier of S is non empty set

T is set

A1 is Element of the carrier of S

A2 is Element of the carrier of S

[A2,T] is set

{A2,T} is non empty set

{A2} is non empty trivial V49(1) set

{{A2,T},{A2}} is non empty set

field the InternalRel of S is set

dom the InternalRel of S is set

rng the InternalRel of S is set

(dom the InternalRel of S) \/ (rng the InternalRel of S) is set

the carrier of S \/ the carrier of S is set

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

A1 is Element of the carrier of (S)

A2 is Element of the carrier of (S)

{A1,A2} is non empty set

A1 "\/" A2 is Element of the carrier of (S)

a is Element of the carrier of (S)

A1 \/ A2 is set

f is Element of the carrier of (S)

a is Element of the carrier of (S)

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

A1 is Element of the carrier of (S)

A2 is Element of the carrier of (S)

{A1,A2} is non empty set

A1 "/\" A2 is Element of the carrier of (S)

a is Element of the carrier of (S)

A1 /\ A2 is set

f is Element of the carrier of (S)

a is Element of the carrier of (S)

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

Bottom (S) is Element of the carrier of (S)

the carrier of (S) is non empty set

A1 is Element of the carrier of (S)

T is Element of the carrier of (S)

"\/" ({},(S)) is Element of the carrier of (S)

S is non empty set

union S is set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

Top (S) is Element of the carrier of (S)

the carrier of (S) is non empty set

A1 is Element of the carrier of (S)

T is Element of the carrier of (S)

"/\" ({},(S)) is Element of the carrier of (S)

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

union S is set

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is set

A2 is set

a is Element of the carrier of (S)

S is non empty set

(S) is non empty strict V84() reflexive transitive antisymmetric RelStr

(S) is non empty Relation-like S -defined S -valued reflexive antisymmetric transitive V34(S) Element of bool [:S,S:]

[:S,S:] is non empty set

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

RelStr(# S,(S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

meet S is set

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is set

A2 is set

a is Element of the carrier of (S)

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

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

bool S is non empty set

bool (bool S) is non empty set

T is Element of the carrier of (S)

A1 is Element of the carrier of (S)

T /\ A1 is set

T \/ A1 is set

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

T is Element of the carrier of (S)

A1 is Element of the carrier of (S)

T "\/" A1 is Element of the carrier of (S)

T \/ A1 is set

T "/\" A1 is Element of the carrier of (S)

T /\ A1 is set

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

bool S is non empty set

bool (bool S) is non empty set

((bool S)) is non empty strict V84() reflexive transitive antisymmetric RelStr

((bool S)) is non empty Relation-like bool S -defined bool S -valued reflexive antisymmetric transitive V34( bool S) Element of bool [:(bool S),(bool S):]

[:(bool S),(bool S):] is non empty set

bool [:(bool S),(bool S):] is non empty set

RelStr(# (bool S),((bool S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of ((bool S)) is non empty set

A2 is Element of the carrier of ((bool S))

a is Element of the carrier of ((bool S))

A2 "/\" a is Element of the carrier of ((bool S))

A2 /\ a is set

A2 "\/" a is Element of the carrier of ((bool S))

A2 \/ a is set

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

Bottom (S) is Element of the carrier of (S)

the carrier of (S) is non empty set

"\/" ({},(LattPOSet (BooleLatt S))) is Element of the carrier of (LattPOSet (BooleLatt S))

the carrier of (LattPOSet (BooleLatt S)) is non empty set

"\/" ({},(BooleLatt S)) is Element of the carrier of (BooleLatt S)

Bottom (BooleLatt S) is Element of the carrier of (BooleLatt S)

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

Top (S) is Element of the carrier of (S)

the carrier of (S) is non empty set

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

bool S is non empty set

bool (bool S) is non empty set

((bool S)) is non empty strict V84() reflexive transitive antisymmetric RelStr

((bool S)) is non empty Relation-like bool S -defined bool S -valued reflexive antisymmetric transitive V34( bool S) Element of bool [:(bool S),(bool S):]

[:(bool S),(bool S):] is non empty set

bool [:(bool S),(bool S):] is non empty set

RelStr(# (bool S),((bool S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

Top ((bool S)) is Element of the carrier of ((bool S))

the carrier of ((bool S)) is non empty set

union (bool S) is Element of bool S

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

bool the carrier of (S) is non empty set

A1 is non empty Element of bool the carrier of (S)

"/\" (A1,(S)) is Element of the carrier of (S)

meet A1 is set

the Element of A1 is Element of A1

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

bool S is non empty set

bool (bool S) is non empty set

f is Element of the carrier of (S)

x9 is set

f is Element of the carrier of (S)

a is Element of the carrier of (S)

f is Element of the carrier of (S)

S is set

(S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

BooleLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V103() complemented Boolean complete LattStr

LattPOSet (BooleLatt S) is non empty strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

the carrier of (BooleLatt S) is non empty set

K167((BooleLatt S)) is Relation-like the carrier of (BooleLatt S) -defined the carrier of (BooleLatt S) -valued reflexive antisymmetric transitive V34( the carrier of (BooleLatt S)) Element of bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):]

[: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

bool [: the carrier of (BooleLatt S), the carrier of (BooleLatt S):] is non empty set

RelStr(# the carrier of (BooleLatt S),K167((BooleLatt S)) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of (S) is non empty set

bool the carrier of (S) is non empty set

A1 is Element of bool the carrier of (S)

"\/" (A1,(S)) is Element of the carrier of (S)

union A1 is set

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

bool S is non empty set

bool (bool S) is non empty set

union (bool S) is Element of bool S

a is Element of the carrier of (S)

f is set

x9 is Element of the carrier of (S)

A2 is Element of the carrier of (S)

a is Element of the carrier of (S)

S is non empty TopSpace-like TopStruct

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr

( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]

[: the topology of S, the topology of S:] is non empty set

bool [: the topology of S, the topology of S:] is non empty set

RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of ( the topology of S) is non empty set

bool the carrier of ( the topology of S) is non empty set

A1 is Element of bool the carrier of ( the topology of S)

"\/" (A1,( the topology of S)) is Element of the carrier of ( the topology of S)

union A1 is set

A2 is Element of bool (bool the carrier of S)

union A2 is Element of bool the carrier of S

f is Element of the carrier of ( the topology of S)

x9 is set

f is Element of the carrier of ( the topology of S)

a is Element of the carrier of ( the topology of S)

f is Element of the carrier of ( the topology of S)

S is non empty TopSpace-like TopStruct

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr

( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]

[: the topology of S, the topology of S:] is non empty set

bool [: the topology of S, the topology of S:] is non empty set

RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

Bottom ( the topology of S) is Element of the carrier of ( the topology of S)

the carrier of ( the topology of S) is non empty set

S is non empty TopSpace-like TopStruct

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr

( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]

[: the topology of S, the topology of S:] is non empty set

bool [: the topology of S, the topology of S:] is non empty set

RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of ( the topology of S) is non empty set

A1 is Element of the carrier of ( the topology of S)

A2 is Element of the carrier of ( the topology of S)

a is Element of the carrier of ( the topology of S)

A2 is Element of the carrier of ( the topology of S)

S is non empty TopSpace-like TopStruct

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr

( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]

[: the topology of S, the topology of S:] is non empty set

bool [: the topology of S, the topology of S:] is non empty set

RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

Top ( the topology of S) is Element of the carrier of ( the topology of S)

the carrier of ( the topology of S) is non empty set

"/\" ({},( the topology of S)) is Element of the carrier of ( the topology of S)

A2 is Element of the carrier of ( the topology of S)

a is Element of the carrier of ( the topology of S)

S is non empty TopSpace-like TopStruct

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr

( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]

[: the topology of S, the topology of S:] is non empty set

bool [: the topology of S, the topology of S:] is non empty set

RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

A1 is V84() reflexive transitive antisymmetric lower-bounded RelStr

the carrier of A1 is set

bool the carrier of A1 is non empty set

A2 is Element of bool the carrier of A1

union A2 is set

f is Element of bool (bool the carrier of S)

the carrier of ( the topology of S) is non empty set

x9 is Element of the carrier of ( the topology of S)

f is Element of the carrier of ( the topology of S)

z is set

x1 is Element of the carrier of ( the topology of S)

f is Element of the carrier of ( the topology of S)

S is non empty TopSpace-like TopStruct

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr

( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]

[: the topology of S, the topology of S:] is non empty set

bool [: the topology of S, the topology of S:] is non empty set

RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of ( the topology of S) is non empty set

A1 is Element of the carrier of ( the topology of S)

A2 is Element of the carrier of ( the topology of S)

S is non empty TopSpace-like TopStruct

the topology of S is non empty Element of bool (bool the carrier of S)

the carrier of S is non empty set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr

( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]

[: the topology of S, the topology of S:] is non empty set

bool [: the topology of S, the topology of S:] is non empty set

RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

S is TopSpace-like TopStruct

the carrier of S is set

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

the topology of S is non empty Element of bool (bool the carrier of S)

( the topology of S) is non empty strict V84() reflexive transitive antisymmetric RelStr

( the topology of S) is non empty Relation-like the topology of S -defined the topology of S -valued reflexive antisymmetric transitive V34( the topology of S) Element of bool [: the topology of S, the topology of S:]

[: the topology of S, the topology of S:] is non empty set

bool [: the topology of S, the topology of S:] is non empty set

RelStr(# the topology of S,( the topology of S) #) is non empty strict V84() reflexive transitive antisymmetric RelStr

the carrier of ( the topology of S) is non empty set

bool the carrier of ( the topology of S) is non empty set

T is Element of bool (bool the carrier of S)

A1 is set

A2 is Element of bool the carrier of S

A1 is Element of bool the carrier of S

S is Relation-like Function-like set

T is set

dom S is set

S . T is set

rng S is set

S is set

the RelStr is RelStr

S --> the RelStr is Relation-like S -defined { the RelStr } -valued Function-like constant V34(S) quasi_total Element of bool [:S,{ the RelStr }:]

{ the RelStr } is non empty trivial V49(1) set

[:S,{ the RelStr }:] is set

bool [:S,{ the RelStr }:] is non empty set

A1 is set

rng (S --> the RelStr ) is set

S is non empty set

T is Relation-like S -defined Function-like V34(S) 1-sorted-yielding () set

A1 is Element of S

T . A1 is set

dom T is Element of bool S

bool S is non empty set

T . A1 is 1-sorted

rng T is set

S is set

T is Relation-like S -defined Function-like V34(S) 1-sorted-yielding () set

Carrier T is Relation-like S -defined Function-like V34(S) set

product (Carrier T) is set

[:(product (Carrier T)),(product (Carrier T)):] is set

bool [:(product (Carrier T)),(product (Carrier T)):] is non empty set

A1 is Relation-like product (Carrier T) -defined product (Carrier T) -valued Element of bool [:(product (Carrier T)),(product (Carrier T)):]

RelStr(# (product (Carrier T)),A1 #) is strict RelStr

A2 is strict RelStr

the carrier of A2 is set

a is Element of the carrier of A2

f is Element of the carrier of A2

[a,f] is set

{a,f} is non empty set

{a} is non empty trivial V49(1) set

{{a,f},{a}} is non empty set

the InternalRel of A2 is Relation-like the carrier of A2 -defined the carrier of A2 -valued Element of bool [: the carrier of A2, the carrier of A2:]

[: the carrier of A2, the carrier of A2:] is set

bool [: the carrier of A2, the carrier of A2:] is non empty set

x9 is Relation-like Function-like set

f is Relation-like Function-like set

A1 is strict RelStr

the carrier of A1 is set

A2 is strict RelStr

the carrier of A2 is set

the InternalRel of A1 is Relation-like the carrier of A1 -defined the carrier of A1 -valued Element of bool [: the carrier of A1, the carrier of A1:]

[: the carrier of A1, the carrier of A1:] is set

bool [: the carrier of A1, the carrier of A1:] is non empty set

the InternalRel of A2 is Relation-like the carrier of A2 -defined the carrier of A2 -valued Element of bool [: the carrier of A2, the carrier of A2:]

[: the carrier of A2, the carrier of A2:] is set

bool [: the carrier of A2, the carrier of A2:] is non empty set

a is set

f is set

[a,f] is set

{a,f} is non empty set

{a} is non empty trivial V49(1) set

{{a,f},{a}} is non empty set

x9 is Element of the carrier of A1

f is Element of the carrier of A1

z is Element of the carrier of A2

x1 is Element of the carrier of A2

z1 is Relation-like Function-like set

i is Relation-like Function-like set

x9 is Element of the carrier of A2

f is Element of the carrier of A2

z is Element of the carrier of A1

x1 is Element of the carrier of A1

z1 is Relation-like Function-like set

i is Relation-like Function-like set

S is set

T is RelStr

S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is set

bool [:S,{T}:] is non empty set

A1 is set

rng (S --> T) is set

S is set

T is RelStr

S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

id {{}} is non empty Relation-like {{}} -defined {{}} -valued reflexive symmetric antisymmetric transitive V34({{}}) Element of bool [:{{}},{{}}:]

[:{{}},{{}}:] is non empty set

bool [:{{}},{{}}:] is non empty set

RelStr(# {{}},(id {{}}) #) is non empty trivial V57() 1 -element strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

S is Relation-like {} -defined Function-like V34( {} ) 1-sorted-yielding () set

({},S) is strict RelStr

the carrier of ({},S) is set

Carrier S is Relation-like {} -defined Function-like V34( {} ) set

product (Carrier S) is set

the InternalRel of ({},S) is Relation-like the carrier of ({},S) -defined the carrier of ({},S) -valued Element of bool [: the carrier of ({},S), the carrier of ({},S):]

[: the carrier of ({},S), the carrier of ({},S):] is set

bool [: the carrier of ({},S), the carrier of ({},S):] is non empty set

a is set

f is set

[a,f] is set

{a,f} is non empty set

{a} is non empty trivial V49(1) set

{{a,f},{a}} is non empty set

A1 is Element of the carrier of ({},S)

{} --> {{}} is empty Relation-like non-empty {} -defined {{{}}} -valued V12() V13() V14() V16() V17() V18() Function-like constant V34( {} ) quasi_total V42() V47() V49( {} ) Function-yielding V131() Element of bool [:{},{{{}}}:]

{{{}}} is non empty trivial V49(1) set

[:{},{{{}}}:] is set

bool [:{},{{{}}}:] is non empty set

A2 is Element of the carrier of ({},S)

x9 is Relation-like Function-like set

f is Relation-like Function-like set

z is set

S . z is set

x9 . z is set

f . z is set

S is RelStr

({},S) is strict RelStr

{} --> S is empty Relation-like {} -defined {S} -valued V12() V13() V14() V16() V17() V18() Function-like constant V34( {} ) quasi_total V42() V47() V49( {} ) Function-yielding V131() 1-sorted-yielding () Element of bool [:{},{S}:]

{S} is non empty trivial V49(1) set

[:{},{S}:] is set

bool [:{},{S}:] is non empty set

({},({} --> S)) is strict RelStr

S is set

T is RelStr

the carrier of T is set

Funcs (S, the carrier of T) is set

(S,T) is strict RelStr

S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

the carrier of (S,T) is set

Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set

dom (Carrier (S --> T)) is Element of bool S

bool S is non empty set

a is set

(Carrier (S --> T)) . a is set

(S --> T) . a is set

f is 1-sorted

the carrier of f is set

product (Carrier (S --> T)) is set

a is set

f is Relation-like Function-like set

dom f is set

rng f is set

x9 is set

(Carrier (S --> T)) . x9 is set

f . x9 is set

a is set

f is Relation-like Function-like set

dom f is set

rng f is set

x9 is set

f is set

f . f is set

(Carrier (S --> T)) . f is set

S is set

T is non empty RelStr

(S,T) is strict RelStr

S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

the carrier of T is non empty set

[:S, the carrier of T:] is set

bool [:S, the carrier of T:] is non empty set

the Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:] is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

Funcs (S, the carrier of T) is non empty FUNCTION_DOMAIN of S, the carrier of T

S is set

T is non empty RelStr

(S,T) is non empty strict RelStr

S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

the carrier of (S,T) is non empty set

the carrier of (S,(S --> T)) is set

the carrier of T is non empty set

[:S, the carrier of T:] is set

bool [:S, the carrier of T:] is non empty set

A1 is Element of the carrier of (S,T)

Funcs (S, the carrier of T) is non empty FUNCTION_DOMAIN of S, the carrier of T

S is set

T is non empty V84() reflexive RelStr

(S,T) is non empty strict RelStr

S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

A1 is non empty set

(A1,T) is non empty strict RelStr

A1 --> T is non empty Relation-like A1 -defined {T} -valued Function-like constant V34(A1) quasi_total 1-sorted-yielding () Element of bool [:A1,{T}:]

[:A1,{T}:] is non empty set

bool [:A1,{T}:] is non empty set

(A1,(A1 --> T)) is strict RelStr

the carrier of (A1,T) is non empty set

A2 is Element of the carrier of (A1,T)

the carrier of T is non empty set

[:A1, the carrier of T:] is non empty set

bool [:A1, the carrier of T:] is non empty set

the carrier of (A1,(A1 --> T)) is set

f is Element of the carrier of (A1,(A1 --> T))

a is Relation-like A1 -defined the carrier of T -valued Function-like quasi_total Element of bool [:A1, the carrier of T:]

x9 is set

(A1 --> T) . x9 is set

a . x9 is set

f is Element of A1

(A1,(A1 --> T),f) is RelStr

z is RelStr

the carrier of z is set

a . f is Element of the carrier of T

x1 is Element of the carrier of z

z1 is Element of the carrier of z

i is Element of the carrier of T

i is Element of the carrier of T

Carrier (A1 --> T) is Relation-like A1 -defined Function-like V34(A1) set

product (Carrier (A1 --> T)) is set

x9 is Relation-like Function-like set

f is Relation-like Function-like set

S is non empty RelStr

({},S) is non empty strict RelStr

{} --> S is empty Relation-like {} -defined {S} -valued V12() V13() V14() V16() V17() V18() Function-like constant V34( {} ) quasi_total V42() V47() V49( {} ) Function-yielding V131() 1-sorted-yielding () Element of bool [:{},{S}:]

{S} is non empty trivial V49(1) set

[:{},{S}:] is set

bool [:{},{S}:] is non empty set

({},({} --> S)) is strict RelStr

S is non empty V84() reflexive RelStr

({},S) is non empty trivial V57() 1 -element strict V84() reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V119() RelStr

{} --> S is empty Relation-like {} -defined {S} -valued V12() V13() V14() V16() V17() V18() Function-like constant V34( {} ) quasi_total V42() V47() V49( {} ) Function-yielding V131() 1-sorted-yielding () Element of bool [:{},{S}:]

{S} is non empty trivial V49(1) set

[:{},{S}:] is set

bool [:{},{S}:] is non empty set

({},({} --> S)) is strict RelStr

S is set

T is non empty transitive RelStr

(S,T) is non empty strict RelStr

S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

the carrier of (S,T) is non empty set

the carrier of (S,(S --> T)) is set

A2 is Element of the carrier of (S,T)

a is Element of the carrier of (S,T)

f is Element of the carrier of (S,T)

f is Element of the carrier of (S,(S --> T))

Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set

product (Carrier (S --> T)) is set

z is Element of the carrier of (S,(S --> T))

x1 is Relation-like Function-like set

z1 is Relation-like Function-like set

x9 is Element of the carrier of (S,(S --> T))

i is Relation-like Function-like set

i is Relation-like Function-like set

the carrier of T is non empty set

[:S, the carrier of T:] is set

bool [:S, the carrier of T:] is non empty set

R is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

yi is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

xi is set

(S --> T) . xi is set

R . xi is set

yi . xi is set

c

c

[:c

bool [:c

J is Element of c

(c

f1 is RelStr

the carrier of f1 is set

R . J is set

yi . J is set

g1 is Element of the carrier of f1

i is Element of the carrier of f1

i . J is set

i . J is set

x1 . J is set

z1 . J is set

i is RelStr

the carrier of i is set

xi is RelStr

the carrier of xi is set

R is Element of the carrier of i

yi is Element of the carrier of i

c

c

R is Relation-like Function-like set

yi is Relation-like Function-like set

S is set

T is non empty antisymmetric RelStr

(S,T) is non empty strict RelStr

S --> T is Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

the carrier of (S,T) is non empty set

the carrier of T is non empty set

[:S, the carrier of T:] is set

bool [:S, the carrier of T:] is non empty set

A2 is Element of the carrier of (S,T)

a is Element of the carrier of (S,T)

the carrier of (S,(S --> T)) is set

z is Element of the carrier of (S,(S --> T))

Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set

product (Carrier (S --> T)) is set

f is Element of the carrier of (S,(S --> T))

x1 is Relation-like Function-like set

z1 is Relation-like Function-like set

i is Relation-like Function-like set

i is Relation-like Function-like set

R is set

(S --> T) . R is set

x1 . R is set

z1 . R is set

yi is RelStr

the carrier of yi is set

xi is Element of the carrier of yi

c

i . R is set

i . R is set

J is RelStr

the carrier of J is set

f1 is Element of the carrier of J

g1 is Element of the carrier of J

f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

f . R is set

x9 is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

x9 . R is set

dom f is Element of bool S

bool S is non empty set

dom x9 is Element of bool S

S is non empty set

T is non empty antisymmetric with_infima RelStr

(S,T) is non empty strict antisymmetric RelStr

S --> T is non empty Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is non empty set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

the carrier of (S,T) is non empty set

A2 is Element of the carrier of (S,T)

a is Element of the carrier of (S,T)

the carrier of T is non empty set

[:S, the carrier of T:] is non empty set

bool [:S, the carrier of T:] is non empty set

x9 is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

f is set

x9 . f is set

f . f is set

z is Element of the carrier of T

x1 is Element of the carrier of T

z "/\" x1 is Element of the carrier of T

z1 is Element of the carrier of T

f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

Funcs (S, the carrier of T) is non empty FUNCTION_DOMAIN of S, the carrier of T

z is Element of the carrier of (S,T)

the carrier of (S,(S --> T)) is set

z1 is Element of the carrier of (S,(S --> T))

x1 is Element of the carrier of (S,(S --> T))

i is set

(S --> T) . i is set

f . i is set

f . i is set

i is Element of S

(S,(S --> T),i) is RelStr

R is RelStr

the carrier of R is set

f . i is Element of the carrier of T

f . i is Element of the carrier of T

yi is Element of the carrier of R

xi is Element of the carrier of R

x9 . i is Element of the carrier of T

c

J is Element of the carrier of T

c

Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set

product (Carrier (S --> T)) is set

i is Relation-like Function-like set

i is Relation-like Function-like set

x1 is Element of the carrier of (S,T)

the carrier of (S,(S --> T)) is set

z1 is Element of the carrier of (S,(S --> T))

i is Element of the carrier of (S,(S --> T))

Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set

product (Carrier (S --> T)) is set

R is Element of the carrier of (S,(S --> T))

c

J is Relation-like Function-like set

i is Element of the carrier of (S,(S --> T))

f1 is Relation-like Function-like set

g1 is Relation-like Function-like set

yi is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

xi is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

i is set

(S --> T) . i is set

yi . i is set

xi . i is set

i is Element of S

(S,(S --> T),i) is RelStr

R is RelStr

the carrier of R is set

yi . i is Element of the carrier of T

xi . i is Element of the carrier of T

yi is Element of the carrier of R

xi is Element of the carrier of R

x9 . i is Element of the carrier of T

f . i is Element of the carrier of T

f . i is Element of the carrier of T

c

J . i is set

f1 . i is set

g1 . i is set

c

the carrier of c

c

the carrier of c

c

c

c

c

c

c

c

i is Relation-like Function-like set

i is Relation-like Function-like set

the carrier of (S,(S --> T)) is set

z1 is Element of the carrier of (S,(S --> T))

x1 is Element of the carrier of (S,(S --> T))

i is set

(S --> T) . i is set

f . i is set

x9 . i is set

i is Element of S

(S,(S --> T),i) is RelStr

R is RelStr

the carrier of R is set

f . i is Element of the carrier of T

x9 . i is Element of the carrier of T

yi is Element of the carrier of R

xi is Element of the carrier of R

f . i is Element of the carrier of T

c

J is Element of the carrier of T

c

Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set

product (Carrier (S --> T)) is set

i is Relation-like Function-like set

i is Relation-like Function-like set

x1 is Element of the carrier of (S,T)

S is non empty set

T is non empty antisymmetric with_suprema RelStr

(S,T) is non empty strict antisymmetric RelStr

S --> T is non empty Relation-like S -defined {T} -valued Function-like constant V34(S) quasi_total 1-sorted-yielding () Element of bool [:S,{T}:]

{T} is non empty trivial V49(1) set

[:S,{T}:] is non empty set

bool [:S,{T}:] is non empty set

(S,(S --> T)) is strict RelStr

the carrier of (S,T) is non empty set

A2 is Element of the carrier of (S,T)

a is Element of the carrier of (S,T)

the carrier of T is non empty set

[:S, the carrier of T:] is non empty set

bool [:S, the carrier of T:] is non empty set

x9 is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

f is set

x9 . f is set

f . f is set

z is Element of the carrier of T

x1 is Element of the carrier of T

z "\/" x1 is Element of the carrier of T

z1 is Element of the carrier of T

f is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

Funcs (S, the carrier of T) is non empty FUNCTION_DOMAIN of S, the carrier of T

z is Element of the carrier of (S,T)

the carrier of (S,(S --> T)) is set

x1 is Element of the carrier of (S,(S --> T))

z1 is Element of the carrier of (S,(S --> T))

i is set

(S --> T) . i is set

f . i is set

f . i is set

i is Element of S

(S,(S --> T),i) is RelStr

R is RelStr

the carrier of R is set

f . i is Element of the carrier of T

f . i is Element of the carrier of T

xi is Element of the carrier of R

yi is Element of the carrier of R

x9 . i is Element of the carrier of T

c

J is Element of the carrier of T

c

Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set

product (Carrier (S --> T)) is set

i is Relation-like Function-like set

i is Relation-like Function-like set

x1 is Element of the carrier of (S,T)

the carrier of (S,(S --> T)) is set

i is Element of the carrier of (S,(S --> T))

Carrier (S --> T) is Relation-like S -defined Function-like V34(S) set

product (Carrier (S --> T)) is set

z1 is Element of the carrier of (S,(S --> T))

yi is Relation-like Function-like set

xi is Relation-like Function-like set

i is Element of the carrier of (S,(S --> T))

R is Element of the carrier of (S,(S --> T))

f1 is Relation-like Function-like set

g1 is Relation-like Function-like set

c

J is Relation-like S -defined the carrier of T -valued Function-like quasi_total Element of bool [:S, the carrier of T:]

i is set

(S --> T) . i is set

c

J . i is set

i is Element of S

(S,(S --> T),i) is RelStr

R is RelStr

the carrier of R is set

J . i is Element of the carrier of T

c

xi is Element of the carrier of R

yi is Element of the carrier of R

x9 . i is Element of the carrier of T

f . i is Element of the carrier of T

f . i is Element of the carrier of T

f1 . i is set

g1 . i is set

yi . i is set

xi . i is set

c

the carrier of c

c

the carrier of c

c