:: LATTICE3 semantic presentation

K118() is set
bool K118() is non empty set
{} is empty set
the empty set is empty set
1 is non empty set
D is set
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
[:(bool D),(bool D):] is non empty set
[:[:(bool D),(bool D):],(bool D):] is non empty set
bool [:[:(bool D),(bool D):],(bool D):] is non empty set
f is Relation-like [:(bool D),(bool D):] -defined bool D -valued Function-like V18([:(bool D),(bool D):], bool D) Element of bool [:[:(bool D),(bool D):],(bool D):]
R is Relation-like [:(bool D),(bool D):] -defined bool D -valued Function-like V18([:(bool D),(bool D):], bool D) Element of bool [:[:(bool D),(bool D):],(bool D):]
LattStr(# (bool D),f,R #) is non empty strict LattStr
the carrier of LattStr(# (bool D),f,R #) is non empty set
the L_join of LattStr(# (bool D),f,R #) is Relation-like [: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):] -defined the carrier of LattStr(# (bool D),f,R #) -valued Function-like V18([: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):], the carrier of LattStr(# (bool D),f,R #)) Element of bool [:[: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):], the carrier of LattStr(# (bool D),f,R #):]
[: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):] is non empty set
[:[: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):], the carrier of LattStr(# (bool D),f,R #):] is non empty set
bool [:[: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):], the carrier of LattStr(# (bool D),f,R #):] is non empty set
the L_meet of LattStr(# (bool D),f,R #) is Relation-like [: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):] -defined the carrier of LattStr(# (bool D),f,R #) -valued Function-like V18([: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):], the carrier of LattStr(# (bool D),f,R #)) Element of bool [:[: the carrier of LattStr(# (bool D),f,R #), the carrier of LattStr(# (bool D),f,R #):], the carrier of LattStr(# (bool D),f,R #):]
R is Element of bool D
A is Element of bool D
the L_join of LattStr(# (bool D),f,R #) . (R,A) is set
R \/ A is Element of bool D
A is Element of bool D
L is Element of bool D
the L_meet of LattStr(# (bool D),f,R #) . (A,L) is set
A /\ L is Element of bool D
f is strict LattStr
the carrier of f is set
the L_join of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V18([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the L_meet of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V18([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
R is strict LattStr
the carrier of R is set
the L_join of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the L_meet of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[:(bool D),(bool D):] is non empty set
[:[:(bool D),(bool D):],(bool D):] is non empty set
bool [:[:(bool D),(bool D):],(bool D):] is non empty set
R is Relation-like [:(bool D),(bool D):] -defined bool D -valued Function-like V18([:(bool D),(bool D):], bool D) Element of bool [:[:(bool D),(bool D):],(bool D):]
X is Element of bool D
Y is Element of bool D
R . (X,Y) is Element of bool D
X \/ Y is Element of bool D
A is Relation-like [:(bool D),(bool D):] -defined bool D -valued Function-like V18([:(bool D),(bool D):], bool D) Element of bool [:[:(bool D),(bool D):],(bool D):]
A . (X,Y) is Element of bool D
A is Relation-like [:(bool D),(bool D):] -defined bool D -valued Function-like V18([:(bool D),(bool D):], bool D) Element of bool [:[:(bool D),(bool D):],(bool D):]
X is Element of bool D
Y is Element of bool D
A . (X,Y) is Element of bool D
X /\ Y is Element of bool D
L is Relation-like [:(bool D),(bool D):] -defined bool D -valued Function-like V18([:(bool D),(bool D):], bool D) Element of bool [:[:(bool D),(bool D):],(bool D):]
L . (X,Y) is Element of bool D
D is set
(D) is strict LattStr
the carrier of (D) is set
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
D is set
(D) is non empty strict LattStr
the carrier of (D) is non empty set
f is Element of the carrier of (D)
R is set
R is Element of the carrier of (D)
A is set
f "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (f,R) is Element of the carrier of (D)
R \/ A is set
bool D is non empty set
A is Element of bool D
L is Element of bool D
H₂((D)) . (A,L) is set
f \/ R is set
f "/\" R is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
the L_meet of (D) . (f,R) is Element of the carrier of (D)
R /\ A is set
bool D is non empty set
A is Element of bool D
L is Element of bool D
H₃((D)) . (A,L) is set
f /\ R is set
D is set
(D) is non empty strict LattStr
the carrier of (D) is non empty set
R is set
(R) is non empty strict LattStr
the carrier of (R) is non empty set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
f "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (f,R) is Element of the carrier of (D)
f \/ R is set
A is Element of the carrier of (R)
A is Element of the carrier of (R)
A "/\" A is Element of the carrier of (R)
the L_meet of (R) is Relation-like [: the carrier of (R), the carrier of (R):] -defined the carrier of (R) -valued Function-like V18([: the carrier of (R), the carrier of (R):], the carrier of (R)) Element of bool [:[: the carrier of (R), the carrier of (R):], the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is non empty set
[:[: the carrier of (R), the carrier of (R):], the carrier of (R):] is non empty set
bool [:[: the carrier of (R), the carrier of (R):], the carrier of (R):] is non empty set
the L_meet of (R) . (A,A) is Element of the carrier of (R)
A /\ A is set
D is set
(D) is non empty strict LattStr
the carrier of (D) is non empty set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
f "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (f,R) is Element of the carrier of (D)
f \/ R is set
D is set
(D) is non empty strict LattStr
the carrier of (D) is non empty set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
f "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (f,R) is Element of the carrier of (D)
f \/ R is set
R "\/" f is Element of the carrier of (D)
the L_join of (D) . (R,f) is Element of the carrier of (D)
R \/ f is set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
R is Element of the carrier of (D)
R "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (R,R) is Element of the carrier of (D)
R \/ R is set
f "\/" (R "\/" R) is Element of the carrier of (D)
the L_join of (D) . (f,(R "\/" R)) is Element of the carrier of (D)
f \/ (R "\/" R) is set
f "\/" R is Element of the carrier of (D)
the L_join of (D) . (f,R) is Element of the carrier of (D)
f \/ R is set
(f "\/" R) "\/" R is Element of the carrier of (D)
the L_join of (D) . ((f "\/" R),R) is Element of the carrier of (D)
(f "\/" R) \/ R is set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
f "/\" R is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_meet of (D) . (f,R) is Element of the carrier of (D)
f /\ R is set
(f "/\" R) "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
the L_join of (D) . ((f "/\" R),R) is Element of the carrier of (D)
(f "/\" R) \/ R is set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
f "/\" R is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_meet of (D) . (f,R) is Element of the carrier of (D)
f /\ R is set
R "/\" f is Element of the carrier of (D)
the L_meet of (D) . (R,f) is Element of the carrier of (D)
R /\ f is set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
R is Element of the carrier of (D)
R "/\" R is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_meet of (D) . (R,R) is Element of the carrier of (D)
R /\ R is set
f "/\" (R "/\" R) is Element of the carrier of (D)
the L_meet of (D) . (f,(R "/\" R)) is Element of the carrier of (D)
f /\ (R "/\" R) is set
f "/\" R is Element of the carrier of (D)
the L_meet of (D) . (f,R) is Element of the carrier of (D)
f /\ R is set
(f "/\" R) "/\" R is Element of the carrier of (D)
the L_meet of (D) . ((f "/\" R),R) is Element of the carrier of (D)
(f "/\" R) /\ R is set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
f "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (f,R) is Element of the carrier of (D)
f \/ R is set
f "/\" (f "\/" R) is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
the L_meet of (D) . (f,(f "\/" R)) is Element of the carrier of (D)
f /\ (f "\/" R) is set
D is set
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Bottom (D) is Element of the carrier of (D)
the carrier of (D) is non empty set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
f "/\" R is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_meet of (D) . (f,R) is Element of the carrier of (D)
f /\ R is set
R is Element of the carrier of (D)
R "/\" f is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_meet of (D) . (R,f) is Element of the carrier of (D)
R /\ f is set
R is Element of the carrier of (D)
f "/\" R is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_meet of (D) . (f,R) is Element of the carrier of (D)
f /\ R is set
R is Element of the carrier of (D)
R "/\" f is Element of the carrier of (D)
the L_meet of (D) . (R,f) is Element of the carrier of (D)
R /\ f is set
D is set
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Top (D) is Element of the carrier of (D)
the carrier of (D) is non empty set
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
f "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (f,R) is Element of the carrier of (D)
f \/ R is set
R is Element of the carrier of (D)
R "\/" f is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (R,f) is Element of the carrier of (D)
R \/ f is set
R is Element of the carrier of (D)
f "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (f,R) is Element of the carrier of (D)
f \/ R is set
R is Element of the carrier of (D)
R "\/" f is Element of the carrier of (D)
the L_join of (D) . (R,f) is Element of the carrier of (D)
R \/ f is set
D is set
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
R is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V81() LattStr
the carrier of R is non empty set
R is Element of the carrier of R
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
D \ R is Element of bool D
A is Element of the carrier of R
A "\/" R is Element of the carrier of R
the L_join of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) commutative associative idempotent Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the L_join of R . (A,R) is Element of the carrier of R
A \/ R is set
D \/ R is set
Top R is Element of the carrier of R
R "\/" A is Element of the carrier of R
the L_join of R . (R,A) is Element of the carrier of R
A "/\" R is Element of the carrier of R
the L_meet of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) commutative associative idempotent Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the L_meet of R . (A,R) is Element of the carrier of R
Bottom R is Element of the carrier of R
R "/\" A is Element of the carrier of R
the L_meet of R . (R,A) is Element of the carrier of R
R "\/" A is Element of the carrier of R
A "/\" R is Element of the carrier of R
A /\ R is set
the carrier of R is non empty set
R is Element of the carrier of R
A is Element of the carrier of R
A is Element of the carrier of R
A "\/" A is Element of the carrier of R
the L_join of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) commutative associative idempotent Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the L_join of R . (A,A) is Element of the carrier of R
R "/\" (A "\/" A) is Element of the carrier of R
the L_meet of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) commutative associative idempotent Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the L_meet of R . (R,(A "\/" A)) is Element of the carrier of R
R "/\" A is Element of the carrier of R
the L_meet of R . (R,A) is Element of the carrier of R
R "/\" A is Element of the carrier of R
the L_meet of R . (R,A) is Element of the carrier of R
(R "/\" A) "\/" (R "/\" A) is Element of the carrier of R
the L_join of R . ((R "/\" A),(R "/\" A)) is Element of the carrier of R
A "\/" A is Element of the carrier of R
R "/\" (A "\/" A) is Element of the carrier of R
the L_meet of R . (R,(A "\/" A)) is Element of the carrier of R
R /\ (A "\/" A) is set
A \/ A is set
R /\ (A \/ A) is set
R /\ A is set
R /\ A is set
(R /\ A) \/ (R /\ A) is set
R "/\" A is Element of the carrier of R
(R "/\" A) \/ (R /\ A) is set
R "/\" A is Element of the carrier of R
(R "/\" A) \/ (R "/\" A) is set
(R "/\" A) "\/" (R "/\" A) is Element of the carrier of R
the L_join of R . ((R "/\" A),(R "/\" A)) is Element of the carrier of R
D is set
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V81() complemented Boolean LattStr
the carrier of (D) is non empty set
R is Element of the carrier of (D)
R ` is Element of the carrier of (D)
D \ R is Element of bool D
bool D is non empty set
(R `) "/\" R is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_meet of (D) . ((R `),R) is Element of the carrier of (D)
(R `) /\ R is set
Bottom (D) is Element of the carrier of (D)
R "\/" (R `) is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
the L_join of (D) . (R,(R `)) is Element of the carrier of (D)
R \/ (R `) is set
Top (D) is Element of the carrier of (D)
R \ R is Element of bool R
bool R is non empty set
(R `) \ R is Element of bool (R `)
bool (R `) is non empty set
(R \ R) \/ ((R `) \ R) is set
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattRel D is Relation-like set
the carrier of D is non empty set
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of D : b<sub>1</sub> [= b<sub>2</sub> } is set
[:H<sub>1</sub>(D),H<sub>1</sub>(D):] is set
f is set
R is set
[f,R] is set
{f,R} is non empty set
{f} is non empty set
{{f,R},{f}} is non empty set
R is Element of the carrier of D
A is Element of the carrier of D
[R,A] is Element of the carrier of [:D,D:]
[:D,D:] is strict LattStr
the carrier of [:D,D:] is set
{R,A} is non empty set
{R} is non empty set
{{R,A},{R}} is non empty set
bool [:H<sub>1</sub>(D),H<sub>1</sub>(D):] is non empty set
f is Relation-like H<sub>1</sub>(D) -defined H<sub>1</sub>(D) -valued Element of bool [:H<sub>1</sub>(D),H<sub>1</sub>(D):]
R is set
[R,R] is set
{R,R} is non empty set
{R} is non empty set
{{R,R},{R}} is non empty set
R is Element of the carrier of D
R is set
R is set
[R,R] is set
{R,R} is non empty set
{R} is non empty set
{{R,R},{R}} is non empty set
[R,R] is set
{R,R} is non empty set
{R} is non empty set
{{R,R},{R}} is non empty set
A is Element of the carrier of D
A is Element of the carrier of D
R is set
R is set
A is set
[R,R] is set
{R,R} is non empty set
{R} is non empty set
{{R,R},{R}} is non empty set
[R,A] is set
{R,A} is non empty set
{R} is non empty set
{{R,A},{R}} is non empty set
[R,A] is set
{R,A} is non empty set
{{R,A},{R}} is non empty set
A is Element of the carrier of D
L is Element of the carrier of D
X is Element of the carrier of D
dom f is Element of bool H<sub>1</sub>(D)
bool H<sub>1</sub>(D) is non empty set
field f is set
dom f is set
rng f is set
(dom f) \/ (rng f) is set
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of D is non empty set
(D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D,(D) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(D) is strict V58() reflexive transitive antisymmetric RelStr
the carrier of D is non empty set
(D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D,(D) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(D) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of D is non empty set
(D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D,(D) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(f) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of f is non empty set
(f) is Relation-like the carrier of f -defined the carrier of f -valued V14( the carrier of f) reflexive antisymmetric transitive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
bool [: the carrier of f, the carrier of f:] is non empty set
RelStr(# the carrier of f,(f) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
LattStr(# the carrier of D, the L_join of D, the L_meet of D #) is non empty strict LattStr
the L_join of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V18([: the carrier of f, the carrier of f:], the carrier of f) commutative associative idempotent Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the L_meet of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V18([: the carrier of f, the carrier of f:], the carrier of f) commutative associative idempotent Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
LattStr(# the carrier of f, the L_join of f, the L_meet of f #) is non empty strict LattStr
[:H<sub>1</sub>(D),H<sub>1</sub>(D):] is set
[:[:H<sub>1</sub>(D),H<sub>1</sub>(D):],H<sub>1</sub>(D):] is set
bool [:[:H<sub>1</sub>(D),H<sub>1</sub>(D):],H<sub>1</sub>(D):] is non empty set
A is Element of the carrier of D
A is Element of the carrier of D
A "\/" A is Element of the carrier of D
the L_join of D . (A,A) is Element of the carrier of D
L is Element of the carrier of f
X is Element of the carrier of f
L "\/" X is Element of the carrier of f
the L_join of f . (L,X) is Element of the carrier of f
A "\/" A is Element of the carrier of D
the L_join of D . (A,A) is Element of the carrier of D
X "\/" L is Element of the carrier of f
the L_join of f . (X,L) is Element of the carrier of f
Y is Element of the carrier of f
[L,Y] is Element of the carrier of [:f,f:]
[:f,f:] is strict LattStr
the carrier of [:f,f:] is set
{L,Y} is non empty set
{L} is non empty set
{{L,Y},{L}} is non empty set
[X,Y] is Element of the carrier of [:f,f:]
{X,Y} is non empty set
{X} is non empty set
{{X,Y},{X}} is non empty set
a is Element of the carrier of D
[A,a] is Element of the carrier of [:D,D:]
[:D,D:] is strict LattStr
the carrier of [:D,D:] is set
{A,a} is non empty set
{A} is non empty set
{{A,a},{A}} is non empty set
[A,a] is Element of the carrier of [:D,D:]
{A,a} is non empty set
{A} is non empty set
{{A,a},{A}} is non empty set
[a,(A "\/" A)] is Element of the carrier of [:D,D:]
{a,(A "\/" A)} is non empty set
{a} is non empty set
{{a,(A "\/" A)},{a}} is non empty set
H<sub>2</sub>(D) . (A,A) is Element of the carrier of D
R is Relation-like [:H<sub>1</sub>(D),H<sub>1</sub>(D):] -defined H<sub>1</sub>(D) -valued Function-like V18([:H<sub>1</sub>(D),H<sub>1</sub>(D):],H<sub>1</sub>(D)) Element of bool [:[:H<sub>1</sub>(D),H<sub>1</sub>(D):],H<sub>1</sub>(D):]
R . (A,A) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A "/\" A is Element of the carrier of D
the L_meet of D . (A,A) is Element of the carrier of D
L is Element of the carrier of f
X is Element of the carrier of f
L "/\" X is Element of the carrier of f
the L_meet of f . (L,X) is Element of the carrier of f
A "/\" A is Element of the carrier of D
the L_meet of D . (A,A) is Element of the carrier of D
X "/\" L is Element of the carrier of f
the L_meet of f . (X,L) is Element of the carrier of f
Y is Element of the carrier of f
[Y,L] is Element of the carrier of [:f,f:]
{Y,L} is non empty set
{Y} is non empty set
{{Y,L},{Y}} is non empty set
[Y,X] is Element of the carrier of [:f,f:]
{Y,X} is non empty set
{{Y,X},{Y}} is non empty set
a is Element of the carrier of D
[a,A] is Element of the carrier of [:D,D:]
{a,A} is non empty set
{a} is non empty set
{{a,A},{a}} is non empty set
[a,A] is Element of the carrier of [:D,D:]
{a,A} is non empty set
{{a,A},{a}} is non empty set
[(A "/\" A),a] is Element of the carrier of [:D,D:]
{(A "/\" A),a} is non empty set
{(A "/\" A)} is non empty set
{{(A "/\" A),a},{(A "/\" A)}} is non empty set
H<sub>3</sub>(D) . (A,A) is Element of the carrier of D
R is Relation-like [:H<sub>1</sub>(D),H<sub>1</sub>(D):] -defined H<sub>1</sub>(D) -valued Function-like V18([:H<sub>1</sub>(D),H<sub>1</sub>(D):],H<sub>1</sub>(D)) Element of bool [:[:H<sub>1</sub>(D),H<sub>1</sub>(D):],H<sub>1</sub>(D):]
R . (A,A) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of D is non empty set
f is Element of the carrier of D
(D) is non empty strict V58() reflexive transitive antisymmetric RelStr
(D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D,(D) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of (D) is non empty set
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(D) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of D is non empty set
(D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D,(D) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of (D) is non empty set
f is Element of the carrier of (D)
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of D is non empty set
(D) is non empty strict V58() reflexive transitive antisymmetric RelStr
(D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D,(D) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
f is Element of the carrier of D
(D,f) is Element of the carrier of (D)
the carrier of (D) is non empty set
R is Element of the carrier of D
(D,R) is Element of the carrier of (D)
[f,R] is Element of the carrier of [:D,D:]
[:D,D:] is strict LattStr
the carrier of [:D,D:] is set
{f,R} is non empty set
{f} is non empty set
{{f,R},{f}} is non empty set
D is set
[:D,D:] is set
bool [:D,D:] is non empty set
f is Relation-like D -defined D -valued V14(D) reflexive antisymmetric transitive Element of bool [:D,D:]
f ~ is Relation-like reflexive antisymmetric transitive set
dom f is Element of bool D
bool D is non empty set
f ~ is Relation-like D -defined D -valued reflexive antisymmetric transitive Element of bool [:D,D:]
dom (f ~) is Element of bool D
D is RelStr
the carrier of D is set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
the InternalRel of D ~ is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the InternalRel of D ~) #) is strict RelStr
D is V58() reflexive transitive antisymmetric RelStr
(D) is strict RelStr
the carrier of D is set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
the InternalRel of D ~ is Relation-like the carrier of D -defined the carrier of D -valued reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the InternalRel of D ~) #) is strict RelStr
( the carrier of D, the InternalRel of D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the carrier of D, the InternalRel of D) #) is strict V58() reflexive transitive antisymmetric RelStr
D is non empty RelStr
(D) is strict RelStr
the carrier of D is non empty set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
the InternalRel of D ~ is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the InternalRel of D ~) #) is non empty strict RelStr
D is RelStr
(D) is strict RelStr
the carrier of D is set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
the InternalRel of D ~ is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the InternalRel of D ~) #) is strict RelStr
((D)) is strict RelStr
the carrier of (D) is set
the InternalRel of (D) is Relation-like the carrier of (D) -defined the carrier of (D) -valued Element of bool [: the carrier of (D), the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is set
bool [: the carrier of (D), the carrier of (D):] is non empty set
the InternalRel of (D) ~ is Relation-like the carrier of (D) -defined the carrier of (D) -valued Element of bool [: the carrier of (D), the carrier of (D):]
RelStr(# the carrier of (D),( the InternalRel of (D) ~) #) is strict RelStr
RelStr(# the carrier of D, the InternalRel of D #) is strict RelStr
D is RelStr
the carrier of D is set
f is Element of the carrier of D
(D) is strict RelStr
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
the InternalRel of D ~ is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the InternalRel of D ~) #) is strict RelStr
the carrier of (D) is set
D is RelStr
(D) is strict RelStr
the carrier of D is set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
the InternalRel of D ~ is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the InternalRel of D ~) #) is strict RelStr
the carrier of (D) is set
f is Element of the carrier of (D)
D is RelStr
the carrier of D is set
(D) is strict RelStr
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
the InternalRel of D ~ is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the InternalRel of D ~) #) is strict RelStr
f is Element of the carrier of D
(D,f) is Element of the carrier of (D)
the carrier of (D) is set
R is Element of the carrier of D
(D,R) is Element of the carrier of (D)
[f,R] is set
{f,R} is non empty set
{f} is non empty set
{{f,R},{f}} is non empty set
[(D,R),(D,f)] is set
{(D,R),(D,f)} is non empty set
{(D,R)} is non empty set
{{(D,R),(D,f)},{(D,R)}} is non empty set
the InternalRel of (D) is Relation-like the carrier of (D) -defined the carrier of (D) -valued Element of bool [: the carrier of (D), the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is set
bool [: the carrier of (D), the carrier of (D):] is non empty set
D is RelStr
the carrier of D is set
D is RelStr
the carrier of D is set
D is RelStr
the carrier of D is set
the Element of the carrier of D is Element of the carrier of D
R is Element of the carrier of D
[ the Element of the carrier of D,R] is set
{ the Element of the carrier of D,R} is non empty set
{ the Element of the carrier of D} is non empty set
{{ the Element of the carrier of D,R},{ the Element of the carrier of D}} is non empty set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
D is RelStr
the carrier of D is set
the Element of the carrier of D is Element of the carrier of D
R is Element of the carrier of D
[R, the Element of the carrier of D] is set
{R, the Element of the carrier of D} is non empty set
{R} is non empty set
{{R, the Element of the carrier of D},{R}} is non empty set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
D is RelStr
(D) is strict RelStr
the carrier of D is set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
the InternalRel of D ~ is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
RelStr(# the carrier of D,( the InternalRel of D ~) #) is strict RelStr
the carrier of (D) is set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
(D,f) is Element of the carrier of D
(D,R) is Element of the carrier of D
R is Element of the carrier of D
(D,R) is Element of the carrier of (D)
A is Element of the carrier of (D)
(D,(D,f)) is Element of the carrier of (D)
(D,(D,R)) is Element of the carrier of (D)
A is Element of the carrier of (D)
(D,A) is Element of the carrier of D
(D,(D,A)) is Element of the carrier of (D)
the carrier of (D) is set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f) is Element of the carrier of (D)
(D,R) is Element of the carrier of (D)
R is Element of the carrier of (D)
(D,R) is Element of the carrier of D
A is Element of the carrier of D
(D,(D,R)) is Element of the carrier of (D)
A is Element of the carrier of D
(D,A) is Element of the carrier of (D)
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(D) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of D is non empty set
(D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D,(D) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of (D) is non empty set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
(D,f) is Element of the carrier of D
(D,R) is Element of the carrier of D
(D,f) "\/" (D,R) is Element of the carrier of D
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_join of D . ((D,f),(D,R)) is Element of the carrier of D
(D,((D,f) "\/" (D,R))) is Element of the carrier of (D)
R is Element of the carrier of (D)
(D,R) "\/" (D,f) is Element of the carrier of D
the L_join of D . ((D,R),(D,f)) is Element of the carrier of D
(D,(D,f)) is Element of the carrier of (D)
(D,(D,R)) is Element of the carrier of (D)
A is Element of the carrier of (D)
(D,A) is Element of the carrier of D
(D,(D,A)) is Element of the carrier of (D)
the carrier of (D) is non empty set
f is Element of the carrier of (D)
R is Element of the carrier of (D)
(D,f) is Element of the carrier of D
(D,R) is Element of the carrier of D
(D,f) "/\" (D,R) is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . ((D,f),(D,R)) is Element of the carrier of D
(D,((D,f) "/\" (D,R))) is Element of the carrier of (D)
R is Element of the carrier of (D)
(D,R) "/\" (D,f) is Element of the carrier of D
the L_meet of D . ((D,R),(D,f)) is Element of the carrier of D
(D,(D,f)) is Element of the carrier of (D)
(D,(D,R)) is Element of the carrier of (D)
A is Element of the carrier of (D)
(D,A) is Element of the carrier of D
(D,(D,A)) is Element of the carrier of (D)
the set is set
{ the set } is non empty set
[:{ the set },{ the set }:] is non empty set
bool [:{ the set },{ the set }:] is non empty set
the Relation-like { the set } -defined { the set } -valued V14({ the set }) reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:] is Relation-like { the set } -defined { the set } -valued V14({ the set }) reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:]
RelStr(# { the set }, the Relation-like { the set } -defined { the set } -valued V14({ the set }) reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:] #) is non empty strict V58() reflexive transitive antisymmetric RelStr
R is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of R is non empty set
A is Element of the carrier of R
A is set
L is Element of the carrier of R
X is Element of the carrier of R
X is Element of the carrier of R
D is non empty RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
{f,R} is non empty Element of bool the carrier of D
bool the carrier of D is non empty set
R is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
f is Element of the carrier of D
R is Element of the carrier of D
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of D : ( b<sub>1</sub> <= f & b<sub>1</sub> <= R ) } is set
A is Element of the carrier of D
A is Element of the carrier of D
L is Element of the carrier of D
A is Element of the carrier of D
L is Element of the carrier of D
A is Element of the carrier of D
the non empty strict V58() reflexive transitive antisymmetric () RelStr is non empty strict V58() reflexive transitive antisymmetric () RelStr
D is RelStr
the carrier of D is set
f is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
D is non empty antisymmetric () RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f,R) is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
L is Element of the carrier of D
D is RelStr
the carrier of D is set
f is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
D is non empty antisymmetric () RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f,R) is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
L is Element of the carrier of D
D is non empty antisymmetric () RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f,R) is Element of the carrier of D
(D,R,f) is Element of the carrier of D
R is Element of the carrier of D
D is non empty antisymmetric () RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f,R) is Element of the carrier of D
R is Element of the carrier of D
(D,(D,f,R),R) is Element of the carrier of D
(D,R,R) is Element of the carrier of D
(D,f,(D,R,R)) is Element of the carrier of D
A is Element of the carrier of D
D is non empty antisymmetric () RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f,R) is Element of the carrier of D
(D,R,f) is Element of the carrier of D
R is Element of the carrier of D
D is non empty antisymmetric () RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f,R) is Element of the carrier of D
R is Element of the carrier of D
(D,(D,f,R),R) is Element of the carrier of D
(D,R,R) is Element of the carrier of D
(D,f,(D,R,R)) is Element of the carrier of D
A is Element of the carrier of D
D is non empty antisymmetric () RelStr
the carrier of D is non empty set
R is Element of the carrier of D
A is Element of the carrier of D
(D,R,A) is Element of the carrier of D
(D,A,R) is Element of the carrier of D
D is non empty antisymmetric () RelStr
the carrier of D is non empty set
R is Element of the carrier of D
A is Element of the carrier of D
(D,R,A) is Element of the carrier of D
(D,A,R) is Element of the carrier of D
D is non empty V58() reflexive antisymmetric () () RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f,R) is Element of the carrier of D
(D,(D,f,R),R) is Element of the carrier of D
R is Element of the carrier of D
D is non empty V58() reflexive antisymmetric () () RelStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
(D,f,R) is Element of the carrier of D
(D,f,(D,f,R)) is Element of the carrier of D
R is Element of the carrier of D
D is non empty V58() reflexive transitive antisymmetric () () RelStr
the carrier of D is non empty set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D, the InternalRel of D #) is non empty strict V58() reflexive transitive antisymmetric RelStr
f is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
(D,R,A) is Element of the carrier of D
A is Element of the carrier of D
L is Element of the carrier of D
(D,A,L) is Element of the carrier of D
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
f is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
R is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
(D,A,A) is Element of the carrier of D
L is Element of the carrier of D
X is Element of the carrier of D
(D,L,X) is Element of the carrier of D
R is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
LattStr(# the carrier of D,f,R #) is non empty strict LattStr
the carrier of LattStr(# the carrier of D,f,R #) is non empty set
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
L is Element of the carrier of D
X is Element of the carrier of D
f . (L,X) is Element of the carrier of D
(D,L,X) is Element of the carrier of D
A "\/" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_join of LattStr(# the carrier of D,f,R #) is Relation-like [: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):] -defined the carrier of LattStr(# the carrier of D,f,R #) -valued Function-like V18([: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):], the carrier of LattStr(# the carrier of D,f,R #)) Element of bool [:[: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):], the carrier of LattStr(# the carrier of D,f,R #):]
[: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):] is non empty set
[:[: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):], the carrier of LattStr(# the carrier of D,f,R #):] is non empty set
bool [:[: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):], the carrier of LattStr(# the carrier of D,f,R #):] is non empty set
the L_join of LattStr(# the carrier of D,f,R #) . (A,A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "\/" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_join of LattStr(# the carrier of D,f,R #) . (A,A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
L is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "\/" L is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_join of LattStr(# the carrier of D,f,R #) . (A,L) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "\/" (A "\/" L) is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_join of LattStr(# the carrier of D,f,R #) . (A,(A "\/" L)) is Element of the carrier of LattStr(# the carrier of D,f,R #)
X is Element of the carrier of D
Y is Element of the carrier of D
a is Element of the carrier of D
(D,Y,a) is Element of the carrier of D
f . (X,(D,Y,a)) is Element of the carrier of D
(D,X,(D,Y,a)) is Element of the carrier of D
(D,X,Y) is Element of the carrier of D
(D,(D,X,Y),a) is Element of the carrier of D
f . ((D,X,Y),a) is Element of the carrier of D
A "\/" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_join of LattStr(# the carrier of D,f,R #) . (A,A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
(A "\/" A) "\/" L is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_join of LattStr(# the carrier of D,f,R #) . ((A "\/" A),L) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "/\" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_meet of LattStr(# the carrier of D,f,R #) is Relation-like [: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):] -defined the carrier of LattStr(# the carrier of D,f,R #) -valued Function-like V18([: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):], the carrier of LattStr(# the carrier of D,f,R #)) Element of bool [:[: the carrier of LattStr(# the carrier of D,f,R #), the carrier of LattStr(# the carrier of D,f,R #):], the carrier of LattStr(# the carrier of D,f,R #):]
the L_meet of LattStr(# the carrier of D,f,R #) . (A,A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
(A "/\" A) "\/" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_join of LattStr(# the carrier of D,f,R #) . ((A "/\" A),A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
L is Element of the carrier of D
X is Element of the carrier of D
(D,L,X) is Element of the carrier of D
f . ((D,L,X),X) is Element of the carrier of D
(D,(D,L,X),X) is Element of the carrier of D
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
L is Element of the carrier of D
X is Element of the carrier of D
R . (L,X) is Element of the carrier of D
(D,L,X) is Element of the carrier of D
A "/\" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_meet of LattStr(# the carrier of D,f,R #) . (A,A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "/\" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_meet of LattStr(# the carrier of D,f,R #) . (A,A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
L is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "/\" L is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_meet of LattStr(# the carrier of D,f,R #) . (A,L) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "/\" (A "/\" L) is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_meet of LattStr(# the carrier of D,f,R #) . (A,(A "/\" L)) is Element of the carrier of LattStr(# the carrier of D,f,R #)
X is Element of the carrier of D
Y is Element of the carrier of D
a is Element of the carrier of D
(D,Y,a) is Element of the carrier of D
R . (X,(D,Y,a)) is Element of the carrier of D
(D,X,(D,Y,a)) is Element of the carrier of D
(D,X,Y) is Element of the carrier of D
(D,(D,X,Y),a) is Element of the carrier of D
R . ((D,X,Y),a) is Element of the carrier of D
A "/\" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_meet of LattStr(# the carrier of D,f,R #) . (A,A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
(A "/\" A) "/\" L is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_meet of LattStr(# the carrier of D,f,R #) . ((A "/\" A),L) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
A is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "\/" A is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_join of LattStr(# the carrier of D,f,R #) . (A,A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
A "/\" (A "\/" A) is Element of the carrier of LattStr(# the carrier of D,f,R #)
the L_meet of LattStr(# the carrier of D,f,R #) . (A,(A "\/" A)) is Element of the carrier of LattStr(# the carrier of D,f,R #)
L is Element of the carrier of D
X is Element of the carrier of D
(D,L,X) is Element of the carrier of D
R . (L,(D,L,X)) is Element of the carrier of D
(D,L,(D,L,X)) is Element of the carrier of D
A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(A) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of A is non empty set
(A) is Relation-like the carrier of A -defined the carrier of A -valued V14( the carrier of A) reflexive antisymmetric transitive Element of bool [: the carrier of A, the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty set
bool [: the carrier of A, the carrier of A:] is non empty set
RelStr(# the carrier of A,(A) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of A : b<sub>1</sub> [= b<sub>2</sub> } is set
A is set
L is set
[A,L] is set
{A,L} is non empty set
{A} is non empty set
{{A,L},{A}} is non empty set
X is Element of the carrier of A
Y is Element of the carrier of A
[X,Y] is Element of the carrier of [:A,A:]
[:A,A:] is strict LattStr
the carrier of [:A,A:] is set
{X,Y} is non empty set
{X} is non empty set
{{X,Y},{X}} is non empty set
a is Element of the carrier of D
p is Element of the carrier of D
(D,a,p) is Element of the carrier of D
X "\/" Y is Element of the carrier of A
the L_join of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) commutative associative idempotent Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
the L_join of A . (X,Y) is Element of the carrier of A
X is set
Y is set
[X,Y] is set
{X,Y} is non empty set
{X} is non empty set
{{X,Y},{X}} is non empty set
a is Element of the carrier of D
p is Element of the carrier of D
(D,a,p) is Element of the carrier of D
q is Element of the carrier of A
y is Element of the carrier of A
q "\/" y is Element of the carrier of A
the L_join of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) commutative associative idempotent Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
the L_join of A . (q,y) is Element of the carrier of A
D is RelStr
the carrier of D is set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D, the InternalRel of D #) is strict RelStr
f is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(f) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of f is non empty set
(f) is Relation-like the carrier of f -defined the carrier of f -valued V14( the carrier of f) reflexive antisymmetric transitive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
bool [: the carrier of f, the carrier of f:] is non empty set
RelStr(# the carrier of f,(f) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
R is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(R) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of R is non empty set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V14( the carrier of R) reflexive antisymmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
RelStr(# the carrier of R,(R) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of D is non empty set
(D) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
( the carrier of D,(D)) is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
D .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
((D .:)) is Relation-like the carrier of (D .:) -defined the carrier of (D .:) -valued V14( the carrier of (D .:)) reflexive antisymmetric transitive Element of bool [: the carrier of (D .:), the carrier of (D .:):]
the carrier of (D .:) is non empty set
[: the carrier of (D .:), the carrier of (D .:):] is non empty set
bool [: the carrier of (D .:), the carrier of (D .:):] is non empty set
(D) is non empty strict V58() reflexive transitive antisymmetric RelStr
RelStr(# the carrier of D,(D) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
((D)) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of (D) is non empty set
the InternalRel of (D) is Relation-like the carrier of (D) -defined the carrier of (D) -valued V14( the carrier of (D)) reflexive antisymmetric transitive Element of bool [: the carrier of (D), the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
bool [: the carrier of (D), the carrier of (D):] is non empty set
the InternalRel of (D) ~ is Relation-like the carrier of (D) -defined the carrier of (D) -valued reflexive antisymmetric transitive Element of bool [: the carrier of (D), the carrier of (D):]
RelStr(# the carrier of (D),( the InternalRel of (D) ~) #) is non empty strict RelStr
((D .:)) is non empty strict V58() reflexive transitive antisymmetric RelStr
RelStr(# the carrier of (D .:),((D .:)) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of D : b<sub>1</sub> [= b<sub>2</sub> } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of (D .:) : b<sub>1</sub> [= b<sub>2</sub> } is set
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
LattStr(# H<sub>1</sub>(D),H<sub>3</sub>(D),H<sub>2</sub>(D) #) is strict LattStr
f is set
R is set
[f,R] is set
{f,R} is non empty set
{f} is non empty set
{{f,R},{f}} is non empty set
[R,f] is set
{R,f} is non empty set
{R} is non empty set
{{R,f},{R}} is non empty set
R is Element of the carrier of D
A is Element of the carrier of D
[R,A] is Element of the carrier of [:D,D:]
[:D,D:] is strict LattStr
the carrier of [:D,D:] is set
{R,A} is non empty set
{R} is non empty set
{{R,A},{R}} is non empty set
L is Element of the carrier of (D .:)
A is Element of the carrier of (D .:)
R is Element of the carrier of (D .:)
A is Element of the carrier of (D .:)
[R,A] is Element of the carrier of [:(D .:),(D .:):]
[:(D .:),(D .:):] is strict LattStr
the carrier of [:(D .:),(D .:):] is set
{R,A} is non empty set
{R} is non empty set
{{R,A},{R}} is non empty set
A is Element of the carrier of D
L is Element of the carrier of D
[R,f] is set
{R,f} is non empty set
{R} is non empty set
{{R,f},{R}} is non empty set
D is non empty LattStr
the carrier of D is non empty set
D is non empty LattStr
the carrier of D is non empty set
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
{R,R} is non empty Element of bool the carrier of D
bool the carrier of D is non empty set
R "/\" R is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . (R,R) is Element of the carrier of D
A is Element of the carrier of D
R "/\" R is Element of the carrier of D
the L_meet of D . (R,R) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
{R,R} is non empty Element of bool the carrier of D
bool the carrier of D is non empty set
R "\/" R is Element of the carrier of D
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_join of D . (R,R) is Element of the carrier of D
A is Element of the carrier of D
R "\/" R is Element of the carrier of D
the L_join of D . (R,R) is Element of the carrier of D
D is set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V81() complemented Boolean LattStr
the carrier of f is non empty set
{ (b<sub>1</sub> `) where b₁ is Element of the carrier of f : b₁ in D } is set
R is Element of the carrier of f
R ` is Element of the carrier of f
A is Element of the carrier of f
A is Element of the carrier of f
A ` is Element of the carrier of f
A is Element of the carrier of f
A ` is Element of the carrier of f
(R `) ` is Element of the carrier of f
(A `) ` is Element of the carrier of f
D is set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V81() complemented Boolean LattStr
the carrier of f is non empty set
{ (b<sub>1</sub> `) where b₁ is Element of the carrier of f : b₁ in D } is set
R is Element of the carrier of f
R ` is Element of the carrier of f
A is Element of the carrier of f
A is Element of the carrier of f
A ` is Element of the carrier of f
A is Element of the carrier of f
A ` is Element of the carrier of f
(R `) ` is Element of the carrier of f
(A `) ` is Element of the carrier of f
D is set
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V81() complemented Boolean LattStr
the carrier of (D) is non empty set
R is set
bool D is non empty set
bool D is non empty Element of bool (bool D)
bool (bool D) is non empty set
R /\ (bool D) is Element of bool (bool D)
union (R /\ (bool D)) is Element of bool D
A is Element of the carrier of (D)
A is Element of the carrier of (D)
A is Element of the carrier of (D)
L is set
X is Element of the carrier of (D)
D is set
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V81() complemented Boolean LattStr
D is set
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V81() complemented Boolean () LattStr
the carrier of (D) is non empty set
f is set
R is Element of the carrier of (D)
A is Element of the carrier of (D)
A is Element of the carrier of (D)
{ (A "/\" b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of (D) : b<sub>1</sub> in f } is set
A "/\" R is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_meet of (D) . (A,R) is Element of the carrier of (D)
A /\ R is set
{ (A "/\" b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of (D) : b<sub>1</sub> in f } is set
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
X is set
Y is Element of the carrier of (D)
A "/\" Y is Element of the carrier of (D)
the L_meet of (D) . (A,Y) is Element of the carrier of (D)
A /\ Y is set
union { (A "/\" b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of (D) : b<sub>1</sub> in f } is set
union (bool D) is Element of bool D
f /\ (bool D) is Element of bool (bool D)
union (f /\ (bool D)) is Element of bool D
a is set
p is Element of the carrier of (D)
X is Element of the carrier of (D)
a is Element of the carrier of (D)
a is set
p is Element of the carrier of (D)
A "/\" p is Element of the carrier of (D)
the L_meet of (D) . (A,p) is Element of the carrier of (D)
A /\ p is set
Y is Element of the carrier of (D)
a is Element of the carrier of (D)
a is set
p is set
q is Element of the carrier of (D)
A "/\" q is Element of the carrier of (D)
the L_meet of (D) . (A,q) is Element of the carrier of (D)
A /\ q is set
A "/\" R is Element of the carrier of (D)
D is set
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V81() complemented Boolean () LattStr
the carrier of (D) is non empty set
f is set
R is Element of the carrier of (D)
A is Element of the carrier of (D)
A is Element of the carrier of (D)
{ (A "\/" b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of (D) : b<sub>1</sub> in f } is set
A "\/" R is Element of the carrier of (D)
the L_join of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
the L_join of (D) . (A,R) is Element of the carrier of (D)
A \/ R is set
{ (A "\/" b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of (D) : b<sub>1</sub> in f } is set
{ (b<sub>1</sub> `) where b₁ is Element of the carrier of (D) : b₁ in f } is set
{ (b₁ `) where b<sub>1</sub> is Element of the carrier of (D) : b<sub>1</sub> in { (A "\/" b<sub>1</sub>) where b<sub>2</sub> is Element of the carrier of (D) : b<sub>1</sub> in f } } is set
A ` is Element of the carrier of (D)
{ ((A `) "/\" b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of (D) : b<sub>1</sub> in { (b<sub>1</sub> `) where b₂ is Element of the carrier of (D) : b₁ in f } } is set
p is set
q is Element of the carrier of (D)
(A `) "/\" q is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
the L_meet of (D) . ((A `),q) is Element of the carrier of (D)
(A `) /\ q is set
y is Element of the carrier of (D)
y ` is Element of the carrier of (D)
A "\/" y is Element of the carrier of (D)
the L_join of (D) . (A,y) is Element of the carrier of (D)
A \/ y is set
(A "\/" y) ` is Element of the carrier of (D)
p is set
q is Element of the carrier of (D)
q ` is Element of the carrier of (D)
y is Element of the carrier of (D)
A "\/" y is Element of the carrier of (D)
the L_join of (D) . (A,y) is Element of the carrier of (D)
A \/ y is set
y ` is Element of the carrier of (D)
(A `) "/\" (y `) is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
the L_meet of (D) . ((A `),(y `)) is Element of the carrier of (D)
(A `) /\ (y `) is set
A ` is Element of the carrier of (D)
(A `) ` is Element of the carrier of (D)
R ` is Element of the carrier of (D)
p is Element of the carrier of (D)
p ` is Element of the carrier of (D)
(p `) ` is Element of the carrier of (D)
p is Element of the carrier of (D)
p ` is Element of the carrier of (D)
(p `) ` is Element of the carrier of (D)
(A `) "/\" (R `) is Element of the carrier of (D)
the L_meet of (D) is Relation-like [: the carrier of (D), the carrier of (D):] -defined the carrier of (D) -valued Function-like V18([: the carrier of (D), the carrier of (D):], the carrier of (D)) commutative associative idempotent Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
the L_meet of (D) . ((A `),(R `)) is Element of the carrier of (D)
(A `) /\ (R `) is set
((A `) "/\" (R `)) ` is Element of the carrier of (D)
(A `) ` is Element of the carrier of (D)
(R `) ` is Element of the carrier of (D)
((A `) `) "\/" ((R `) `) is Element of the carrier of (D)
the L_join of (D) . (((A `) `),((R `) `)) is Element of the carrier of (D)
((A `) `) \/ ((R `) `) is set
A "\/" R is Element of the carrier of (D)
the set is set
( the set ) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V81() complemented Boolean () LattStr
D is set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of f is non empty set
(f) is non empty strict V58() reflexive transitive antisymmetric RelStr
(f) is Relation-like the carrier of f -defined the carrier of f -valued V14( the carrier of f) reflexive antisymmetric transitive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
bool [: the carrier of f, the carrier of f:] is non empty set
RelStr(# the carrier of f,(f) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
R is Element of the carrier of f
(f,R) is Element of the carrier of (f)
the carrier of (f) is non empty set
R is Element of the carrier of (f)
(f,R) is Element of the carrier of f
(f,(f,R)) is Element of the carrier of (f)
R is Element of the carrier of f
(f,R) is Element of the carrier of (f)
D is set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(f) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of f is non empty set
(f) is Relation-like the carrier of f -defined the carrier of f -valued V14( the carrier of f) reflexive antisymmetric transitive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
bool [: the carrier of f, the carrier of f:] is non empty set
RelStr(# the carrier of f,(f) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of (f) is non empty set
R is Element of the carrier of (f)
(f,R) is Element of the carrier of f
(f,(f,R)) is Element of the carrier of (f)
D is set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of f is non empty set
(f) is non empty strict V58() reflexive transitive antisymmetric RelStr
(f) is Relation-like the carrier of f -defined the carrier of f -valued V14( the carrier of f) reflexive antisymmetric transitive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
bool [: the carrier of f, the carrier of f:] is non empty set
RelStr(# the carrier of f,(f) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
R is Element of the carrier of f
(f,R) is Element of the carrier of (f)
the carrier of (f) is non empty set
R is Element of the carrier of (f)
(f,R) is Element of the carrier of f
(f,(f,R)) is Element of the carrier of (f)
R is Element of the carrier of f
(f,R) is Element of the carrier of (f)
D is set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(f) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of f is non empty set
(f) is Relation-like the carrier of f -defined the carrier of f -valued V14( the carrier of f) reflexive antisymmetric transitive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
bool [: the carrier of f, the carrier of f:] is non empty set
RelStr(# the carrier of f,(f) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of (f) is non empty set
R is Element of the carrier of (f)
(f,R) is Element of the carrier of f
(f,(f,R)) is Element of the carrier of (f)
D is non empty V58() reflexive transitive antisymmetric () RelStr
(D) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of D is non empty set
the InternalRel of D is Relation-like the carrier of D -defined the carrier of D -valued V14( the carrier of D) reflexive antisymmetric transitive Element of bool [: the carrier of D, the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
bool [: the carrier of D, the carrier of D:] is non empty set
RelStr(# the carrier of D, the InternalRel of D #) is non empty strict V58() reflexive transitive antisymmetric RelStr
((D)) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of (D) is non empty set
((D)) is Relation-like the carrier of (D) -defined the carrier of (D) -valued V14( the carrier of (D)) reflexive antisymmetric transitive Element of bool [: the carrier of (D), the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is non empty set
bool [: the carrier of (D), the carrier of (D):] is non empty set
RelStr(# the carrier of (D),((D)) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
R is set
R is Element of the carrier of D
the carrier of ((D)) is non empty set
A is Element of the carrier of ((D))
((D),A) is Element of the carrier of (D)
A is Element of the carrier of (D)
((D),A) is Element of the carrier of ((D))
L is Element of the carrier of (D)
X is Element of the carrier of D
[X,R] is Element of [: the carrier of D, the carrier of D:]
{X,R} is non empty set
{X} is non empty set
{{X,R},{X}} is non empty set
((D),L) is Element of the carrier of ((D))
L is Element of the carrier of (D)
((D),L) is Element of the carrier of ((D))
X is Element of the carrier of D
Y is Element of the carrier of D
a is Element of the carrier of ((D))
[Y,X] is Element of [: the carrier of D, the carrier of D:]
{Y,X} is non empty set
{Y} is non empty set
{{Y,X},{Y}} is non empty set
the InternalRel of RelStr(# the carrier of D, the InternalRel of D #) is Relation-like the carrier of RelStr(# the carrier of D, the InternalRel of D #) -defined the carrier of RelStr(# the carrier of D, the InternalRel of D #) -valued V14( the carrier of RelStr(# the carrier of D, the InternalRel of D #)) reflexive antisymmetric transitive Element of bool [: the carrier of RelStr(# the carrier of D, the InternalRel of D #), the carrier of RelStr(# the carrier of D, the InternalRel of D #):]
the carrier of RelStr(# the carrier of D, the InternalRel of D #) is non empty set
[: the carrier of RelStr(# the carrier of D, the InternalRel of D #), the carrier of RelStr(# the carrier of D, the InternalRel of D #):] is non empty set
bool [: the carrier of RelStr(# the carrier of D, the InternalRel of D #), the carrier of RelStr(# the carrier of D, the InternalRel of D #):] is non empty set
[R,X] is Element of [: the carrier of D, the carrier of D:]
{R,X} is non empty set
{R} is non empty set
{{R,X},{R}} is non empty set
D is non empty LattStr
the carrier of D is non empty set
f is set
R is Element of the carrier of D
R is Element of the carrier of D
D is non empty LattStr
the carrier of D is non empty set
f is set
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } ) is Element of the carrier of D
D is non empty LattStr
the carrier of D is non empty set
bool the carrier of D is non empty set
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is set
{ (f "/\" b₁) where b₁ is Element of the carrier of D : b₁ in R } is set
(D, { (f "/\" b₁) where b₁ is Element of the carrier of D : b₁ in R } ) is Element of the carrier of D
(D,R) is Element of the carrier of D
f "/\" (D,R) is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . (f,(D,R)) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
f "/\" A is Element of the carrier of D
the L_meet of D . (f,A) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is set
(D,f) is Element of the carrier of D
R is Element of the carrier of D
R "/\" (D,f) is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . (R,(D,f)) is Element of the carrier of D
{ (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } is set
(D, { (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
f is set
R is Element of the carrier of D
R is Element of the carrier of D
{ (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } is set
R "/\" R is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . (R,R) is Element of the carrier of D
A is Element of the carrier of D
{ (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } is set
(D,f) is Element of the carrier of D
(D, { (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) is Element of the carrier of D
R "/\" R is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is set
(D,R) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } ) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
L is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is set
(D,R) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } ) is Element of the carrier of D
f "\/" (D,R) is Element of the carrier of D
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_join of D . (f,(D,R)) is Element of the carrier of D
{ (f "\/" b₁) where b₁ is Element of the carrier of D : b₁ in R } is set
(D, { (f "\/" b₁) where b₁ is Element of the carrier of D : b₁ in R } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁, { (f "\/" b₁) where b₁ is Element of the carrier of D : b₁ in R } ) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁, { (f "\/" b₁) where b₁ is Element of the carrier of D : b₁ in R } ) } ) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
f "\/" A is Element of the carrier of D
the L_join of D . (f,A) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is set
(D,f) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } ) is Element of the carrier of D
R is Element of the carrier of D
{ (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } is set
(D, { (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁, { (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁, { (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) } ) is Element of the carrier of D
R "\/" (D,f) is Element of the carrier of D
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_join of D . (R,(D,f)) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
f is set
R is Element of the carrier of D
R is Element of the carrier of D
{ (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } is set
R "\/" R is Element of the carrier of D
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_join of D . (R,R) is Element of the carrier of D
A is Element of the carrier of D
{ (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } is set
(D,f) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } ) is Element of the carrier of D
(D, { (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁, { (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁, { (R "\/" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) } ) is Element of the carrier of D
R "\/" R is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is set
(D,f) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁, { b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } ) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁, { b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } ) } ) is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
R is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is set
(D,R) is Element of the carrier of D
(D,R) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } ) is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is set
(D,R) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } ) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is set
(D,R) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is set
(D,R) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } ) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
{f} is non empty Element of bool the carrier of D
bool the carrier of D is non empty set
(D,{f}) is Element of the carrier of D
(D,{f}) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,{f}) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,{f}) } ) is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
f "\/" R is Element of the carrier of D
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_join of D . (f,R) is Element of the carrier of D
{f,R} is non empty Element of bool the carrier of D
bool the carrier of D is non empty set
(D,{f,R}) is Element of the carrier of D
f "/\" R is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
the L_meet of D . (f,R) is Element of the carrier of D
(D,{f,R}) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,{f,R}) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,{f,R}) } ) is Element of the carrier of D
R is Element of the carrier of D
R "\/" f is Element of the carrier of D
the L_join of D . (R,f) is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
R "/\" f is Element of the carrier of D
the L_meet of D . (R,f) is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : b₁ [= f } is set
(D, { b₁ where b₁ is Element of the carrier of D : b₁ [= f } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : f [= b₁ } is set
(D, { b₁ where b₁ is Element of the carrier of D : f [= b₁ } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁, { b₁ where b₁ is Element of the carrier of D : f [= b₁ } ) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁, { b₁ where b₁ is Element of the carrier of D : f [= b₁ } ) } ) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
f is set
(D,f) is Element of the carrier of D
the carrier of D is non empty set
(D,f) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } ) is Element of the carrier of D
R is set
(D,R) is Element of the carrier of D
(D,R) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,R) } ) is Element of the carrier of D
R is Element of the carrier of D
R is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is set
(D,f) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : ex b₂ being Element of the carrier of D st
( b₁ [= b₂ & b₂ in f ) } is set
(D, { b₁ where b₁ is Element of the carrier of D : ex b₂ being Element of the carrier of D st
( b₁ [= b₂ & b₂ in f ) } ) is Element of the carrier of D
(D,f) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁,f) } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : ex b₂ being Element of the carrier of D st
( b₂ [= b₁ & b₂ in f ) } is set
(D, { b₁ where b₁ is Element of the carrier of D : ex b₂ being Element of the carrier of D st
( b₂ [= b₁ & b₂ in f ) } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : (D,b₁, { b₁ where b₁ is Element of the carrier of D : ex b₂ being Element of the carrier of D st
( b₂ [= b₁ & b₂ in f ) } ) } is set
(D, { b₁ where b₁ is Element of the carrier of D : (D,b₁, { b₁ where b₁ is Element of the carrier of D : ex b₂ being Element of the carrier of D st
( b₂ [= b₁ & b₂ in f ) } ) } ) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
L is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
L is Element of the carrier of D
A is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is set
(D,f) is Element of the carrier of D
R is set
(D,R) is Element of the carrier of D
R is Element of the carrier of D
A is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is set
union f is set
(D,(union f)) is Element of the carrier of D
{ (D,b₁) where b₁ is Element of bool the carrier of D : b₁ in f } is set
(D, { (D,b₁) where b₁ is Element of bool the carrier of D : b₁ in f } ) is Element of the carrier of D
R is Element of the carrier of D
A is Element of bool the carrier of D
(D,A) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : ex b₂ being Element of the carrier of D st
( b₁ [= b₂ & b₂ in { (D,b₁) where b₃ is Element of bool the carrier of D : b₁ in f } ) } is set
A is set
A is set
X is Element of the carrier of D
L is Element of bool the carrier of D
(D,L) is Element of the carrier of D
(D, { b₁ where b₁ is Element of the carrier of D : ex b₂ being Element of the carrier of D st
( b₁ [= b₂ & b₂ in { (D,b₁) where b₃ is Element of bool the carrier of D : b₁ in f } ) } ) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
Bottom D is Element of the carrier of D
the carrier of D is non empty set
(D,{}) is Element of the carrier of D
f is Element of the carrier of D
(D,{}) "/\" f is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . ((D,{}),f) is Element of the carrier of D
R is Element of the carrier of D
f "/\" (D,{}) is Element of the carrier of D
the L_meet of D . (f,(D,{})) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
Top D is Element of the carrier of D
the carrier of D is non empty set
(D, the carrier of D) is Element of the carrier of D
R is Element of the carrier of D
(D, the carrier of D) "\/" R is Element of the carrier of D
the L_join of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_join of D . ((D, the carrier of D),R) is Element of the carrier of D
R "\/" (D, the carrier of D) is Element of the carrier of D
the L_join of D . (R,(D, the carrier of D)) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
f is Element of the carrier of D
R is Element of the carrier of D
f => R is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : f "/\" b₁ [= R } is set
(D, { b₁ where b₁ is Element of the carrier of D : f "/\" b₁ [= R } ) is Element of the carrier of D
f "/\" (f => R) is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . (f,(f => R)) is Element of the carrier of D
A is Element of the carrier of D
A is Element of the carrier of D
f "/\" A is Element of the carrier of D
the L_meet of D . (f,A) is Element of the carrier of D
D is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
the carrier of D is non empty set
R is Element of the carrier of D
f is set
{ (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } is set
(D,f) is Element of the carrier of D
(D, { (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) is Element of the carrier of D
{ b₁ where b₁ is Element of the carrier of D : R "/\" b₁ [= (D, { (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) } is set
R => (D, { (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) is Element of the carrier of D
X is Element of the carrier of D
R "/\" X is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . (R,X) is Element of the carrier of D
(D, { b₁ where b₁ is Element of the carrier of D : R "/\" b₁ [= (D, { (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } ) } ) is Element of the carrier of D
R "/\" (D,f) is Element of the carrier of D
the L_meet of D is Relation-like [: the carrier of D, the carrier of D:] -defined the carrier of D -valued Function-like V18([: the carrier of D, the carrier of D:], the carrier of D) commutative associative idempotent Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the L_meet of D . (R,(D,f)) is Element of the carrier of D
R "/\" (R => (D, { (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } )) is Element of the carrier of D
the L_meet of D . (R,(R => (D, { (R "/\" b₁) where b₁ is Element of the carrier of D : b₁ in f } ))) is Element of the carrier of D
D is set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () LattStr
the carrier of f is non empty set
(f,D) is Element of the carrier of f
R is Element of the carrier of f
R "/\" (f,D) is Element of the carrier of f
the L_meet of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V18([: the carrier of f, the carrier of f:], the carrier of f) commutative associative idempotent Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the L_meet of f . (R,(f,D)) is Element of the carrier of f
{ (R "/\" b₁) where b₁ is Element of the carrier of f : b₁ in D } is set
(f, { (R "/\" b₁) where b₁ is Element of the carrier of f : b₁ in D } ) is Element of the carrier of f
(f,D) "/\" R is Element of the carrier of f
the L_meet of f . ((f,D),R) is Element of the carrier of f
{ (b₁ "/\" R) where b₁ is Element of the carrier of f : b₁ in D } is set
(f, { (b₁ "/\" R) where b₁ is Element of the carrier of f : b₁ in D } ) is Element of the carrier of f
R is Element of the carrier of f
R "/\" R is Element of the carrier of f
the L_meet of f . (R,R) is Element of the carrier of f
R "/\" R is Element of the carrier of f
the L_meet of f . (R,R) is Element of the carrier of f
{ H₅(b₁) where b₁ is Element of the carrier of f : S₁[b₁] } is set
{ H₄(b₁) where b₁ is Element of the carrier of f : S₁[b₁] } is set
D is set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () () LattStr
the carrier of f is non empty set
(f,D) is Element of the carrier of f
{ b₁ where b₁ is Element of the carrier of f : (f,b₁,D) } is set
(f, { b₁ where b₁ is Element of the carrier of f : (f,b₁,D) } ) is Element of the carrier of f
R is Element of the carrier of f
R "\/" (f,D) is Element of the carrier of f
the L_join of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V18([: the carrier of f, the carrier of f:], the carrier of f) commutative associative idempotent Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the L_join of f . (R,(f,D)) is Element of the carrier of f
{ (R "\/" b₁) where b₁ is Element of the carrier of f : b₁ in D } is set
(f, { (R "\/" b₁) where b₁ is Element of the carrier of f : b₁ in D } ) is Element of the carrier of f
{ b₁ where b₁ is Element of the carrier of f : (f,b₁, { (R "\/" b₁) where b₁ is Element of the carrier of f : b₁ in D } ) } is set
(f, { b₁ where b₁ is Element of the carrier of f : (f,b₁, { (R "\/" b₁) where b₁ is Element of the carrier of f : b₁ in D } ) } ) is Element of the carrier of f
(f,D) "\/" R is Element of the carrier of f
the L_join of f . ((f,D),R) is Element of the carrier of f
{ (b₁ "\/" R) where b₁ is Element of the carrier of f : b₁ in D } is set
(f, { (b₁ "\/" R) where b₁ is Element of the carrier of f : b₁ in D } ) is Element of the carrier of f
{ b₁ where b₁ is Element of the carrier of f : (f,b₁, { (b₁ "\/" R) where b₁ is Element of the carrier of f : b₁ in D } ) } is set
(f, { b₁ where b₁ is Element of the carrier of f : (f,b₁, { (b₁ "\/" R) where b₁ is Element of the carrier of f : b₁ in D } ) } ) is Element of the carrier of f
R is Element of the carrier of f
R "\/" R is Element of the carrier of f
the L_join of f . (R,R) is Element of the carrier of f
R "\/" R is Element of the carrier of f
the L_join of f . (R,R) is Element of the carrier of f
{ H₅(b₁) where b₁ is Element of the carrier of f : S₁[b₁] } is set
{ H₄(b₁) where b₁ is Element of the carrier of f : S₁[b₁] } is set
F₂() is non empty set
F₁() is set
{ F₁() where b₁ is Element of F₂() : P₁[b₁] } is set
{F₁()} is non empty set
D is set
f is Element of F₂()
D is set
f is Element of F₂()
F₂() is non empty set
F₄() is Relation-like Function-like set
dom F₄() is set
F₁() is non empty set
{ F₃(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
F₄() .: { F₃(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
{ (F₄() . F₃(b₁)) where b₁ is Element of F₁() : P₁[b₁] } is set
f is set
R is set
F₄() . R is set
R is Element of F₁()
F₃(R) is Element of F₂()
f is set
R is Element of F₁()
F₃(R) is Element of F₂()
F₄() . F₃(R) is set
D is non empty set
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
[:(bool D),D:] is non empty set
bool [:(bool D),D:] is non empty set
f is Relation-like bool D -defined D -valued Function-like V18( bool D,D) Element of bool [:(bool D),D:]
[:D,D:] is non empty set
bool [:D,D:] is non empty set
R is Relation-like D -defined D -valued Element of bool [:D,D:]
dom f is Element of bool (bool D)
bool (bool D) is non empty set
R is Element of bool D
f . R is Element of D
A is Element of bool D
f . A is Element of D
{(f . R),(f . A)} is non empty Element of bool D
f . {(f . R),(f . A)} is Element of D
{R,A} is non empty Element of bool (bool D)
f .: {R,A} is Element of bool D
f . (f .: {R,A}) is Element of D
union {R,A} is Element of bool D
f . (union {R,A}) is Element of D
R \/ A is Element of bool D
f . (R \/ A) is Element of D
A is Element of D
R is Element of D
{R} is non empty Element of bool D
A is Element of bool D
A \/ {R} is non empty Element of bool D
f . (A \/ {R}) is Element of D
{ (f . {b₁,R}) where b₁ is Element of D : b₁ in A } is set
f . { (f . {b₁,R}) where b₁ is Element of D : b₁ in A } is set
{ {b₁,R} where b₁ is Element of D : b₁ in A } is set
union { {b₁,R} where b₁ is Element of D : b₁ in A } is set
X is set
{X,R} is non empty set
{A,R} is non empty Element of bool D
X is set
Y is set
a is Element of D
{a,R} is non empty Element of bool D
X is set
{ H₄(b₁) where b₁ is Element of D : S₂[b₁] } is set
f .: { H₄(b₁) where b₁ is Element of D : S₂[b₁] } is Element of bool D
{ (f . H₄(b₁)) where b₁ is Element of D : S₂[b₁] } is set
X is Element of bool (bool D)
union X is Element of bool D
f . (union X) is Element of D
R is set
[R,R] is set
{R,R} is non empty set
{R} is non empty set
{{R,R},{R}} is non empty set
f . {R} is set
f . {R,R} is set
R is set
A is set
[R,A] is set
{R,A} is non empty set
{R} is non empty set
{{R,A},{R}} is non empty set
[A,R] is set
{A,R} is non empty set
{A} is non empty set
{{A,R},{A}} is non empty set
f . {R,A} is set
R is set
A is set
A is set
[R,A] is set
{R,A} is non empty set
{R} is non empty set
{{R,A},{R}} is non empty set
[A,A] is set
{A,A} is non empty set
{A} is non empty set
{{A,A},{A}} is non empty set
[R,A] is set
{R,A} is non empty set
{{R,A},{R}} is non empty set
f . {R,A} is set
f . {A,A} is set
L is Element of D
Y is Element of D
{L,Y} is non empty Element of bool D
f . {L,Y} is Element of D
{L} is non empty Element of bool D
f . {L} is Element of D
X is Element of D
{X,Y} is non empty Element of bool D
f . {X,Y} is Element of D
{(f . {L}),(f . {X,Y})} is non empty Element of bool D
f . {(f . {L}),(f . {X,Y})} is Element of D
{L} \/ {X,Y} is non empty Element of bool D
f . ({L} \/ {X,Y}) is Element of D
{L,X,Y} is non empty Element of bool D
f . {L,X,Y} is Element of D
{L,X} is non empty Element of bool D
{Y} is non empty Element of bool D
{L,X} \/ {Y} is non empty Element of bool D
f . ({L,X} \/ {Y}) is Element of D
f . {L,X} is Element of D
f . {Y} is Element of D
{(f . {L,X}),(f . {Y})} is non empty Element of bool D
f . {(f . {L,X}),(f . {Y})} is Element of D
dom R is Element of bool D
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
R is Relation-like D -defined D -valued V14(D) reflexive antisymmetric transitive Element of bool [:D,D:]
RelStr(# D,R #) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of RelStr(# D,R #) is non empty set
A is set
A /\ D is set
L is Element of bool D
f . L is Element of D
X is Element of the carrier of RelStr(# D,R #)
Y is Element of the carrier of RelStr(# D,R #)
{Y} is non empty Element of bool the carrier of RelStr(# D,R #)
bool the carrier of RelStr(# D,R #) is non empty set
{Y} \/ L is non empty set
f . {Y} is set
{(f . {Y}),X} is non empty set
f . {(f . {Y}),X} is set
{Y,X} is non empty Element of bool the carrier of RelStr(# D,R #)
f . {Y,X} is set
[Y,X] is Element of [: the carrier of RelStr(# D,R #), the carrier of RelStr(# D,R #):]
[: the carrier of RelStr(# D,R #), the carrier of RelStr(# D,R #):] is non empty set
{Y,X} is non empty set
{Y} is non empty set
{{Y,X},{Y}} is non empty set
the InternalRel of RelStr(# D,R #) is Relation-like the carrier of RelStr(# D,R #) -defined the carrier of RelStr(# D,R #) -valued V14( the carrier of RelStr(# D,R #)) reflexive antisymmetric transitive Element of bool [: the carrier of RelStr(# D,R #), the carrier of RelStr(# D,R #):]
bool [: the carrier of RelStr(# D,R #), the carrier of RelStr(# D,R #):] is non empty set
Y is Element of the carrier of RelStr(# D,R #)
{X,Y} is non empty Element of bool the carrier of RelStr(# D,R #)
bool the carrier of RelStr(# D,R #) is non empty set
f . {X,Y} is set
{Y} is non empty Element of bool the carrier of RelStr(# D,R #)
f . {Y} is set
{X,(f . {Y})} is non empty set
f . {X,(f . {Y})} is set
L \/ {Y} is non empty set
f . (L \/ {Y}) is set
the Element of L is Element of L
q is Element of D
{q,Y} is non empty set
f . {q,Y} is set
y is Element of the carrier of RelStr(# D,R #)
b is Element of D
[q,b] is Element of [:D,D:]
{q,b} is non empty set
{q} is non empty set
{{q,b},{q}} is non empty set
p is Element of D
{ H₄(b₁) where b₁ is Element of D : S₂[b₁] } is set
{ H₅(b₁) where b₁ is Element of D : S₂[b₁] } is set
{ Y where b₁ is Element of D : S₂[b₁] } is set
[X,Y] is Element of [: the carrier of RelStr(# D,R #), the carrier of RelStr(# D,R #):]
[: the carrier of RelStr(# D,R #), the carrier of RelStr(# D,R #):] is non empty set
{X,Y} is non empty set
{X} is non empty set
{{X,Y},{X}} is non empty set
the InternalRel of RelStr(# D,R #) is Relation-like the carrier of RelStr(# D,R #) -defined the carrier of RelStr(# D,R #) -valued V14( the carrier of RelStr(# D,R #)) reflexive antisymmetric transitive Element of bool [: the carrier of RelStr(# D,R #), the carrier of RelStr(# D,R #):]
bool [: the carrier of RelStr(# D,R #), the carrier of RelStr(# D,R #):] is non empty set
A is non empty strict V58() reflexive transitive antisymmetric () RelStr
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like () LattStr
(L) is non empty strict V58() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
(L) is Relation-like the carrier of L -defined the carrier of L -valued V14( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L,(L) #) is non empty strict V58() reflexive transitive antisymmetric RelStr
bool the carrier of L is non empty set
X is Element of bool the carrier of L
the carrier of (L) is non empty set
Y is Element of bool D
f . Y is Element of D
a is Element of the carrier of (L)
(L,a) is Element of the carrier of L
q is Element of the carrier of (L)
{q} is non empty Element of bool the carrier of (L)
bool the carrier of (L) is non empty set
{q} \/ X is non empty set
y is Element of D
{y,(f . Y)} is non empty Element of bool D
f . {y,(f . Y)} is Element of D
{y} is non empty Element of bool D
f . {y} is Element of D
{(f . {y}),(f . Y)} is non empty Element of bool D
f . {(f . {y}),(f . Y)} is Element of D
[q,a] is Element of [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is non empty set
{q,a} is non empty set
{q} is non empty set
{{q,a},{q}} is non empty set
the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued V14( the carrier of (L)) reflexive antisymmetric transitive Element of bool [: the carrier of (L), the carrier of (L):]
bool [: the carrier of (L), the carrier of (L):] is non empty set
q is Element of the carrier of L
y is Element of D
(L,q) is Element of the carrier of (L)
b is Element of the carrier of (L)
{(f . Y),b} is non empty set
f . {(f . Y),b} is set
{y} is non empty Element of bool D
f . {y} is Element of D
{(f . Y),(f . {y})} is non empty Element of bool D
f . {(f . Y),(f . {y})} is Element of D
{b} is non empty Element of bool the carrier of (L)
bool the carrier of (L) is non empty set
Y \/ {b} is non empty set
f . (Y \/ {b}) is set
the Element of Y is Element of Y
t is Element of D
{t,b} is non empty set
f . {t,b} is set
s is Element of the carrier of (L)
[t,y] is Element of [:D,D:]
{t,y} is non empty set
{t} is non empty set
{{t,y},{t}} is non empty set
s is Element of D
{ H₄(b₁) where b₁ is Element of D : S₂[b₁] } is set
{ H₅(b₁) where b₁ is Element of D : S₂[b₁] } is set
{ b where b₁ is Element of D : S₂[b₁] } is set
{a,b} is non empty Element of bool the carrier of (L)
f . {a,b} is set
f . {b} is set
{a,b} is non empty Element of bool the carrier of (L)
f . {a,b} is set
{a,b} is non empty Element of bool the carrier of (L)
f . {a,b} is set
{a,b} is non empty Element of bool the carrier of (L)
f . {a,b} is set
[a,b] is Element of [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is non empty set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
the InternalRel of (L) is Relation-like the carrier of (L) -defined the carrier of (L) -valued V14( the carrier of (L)) reflexive antisymmetric transitive Element of bool [: the carrier of (L), the carrier of (L):]
bool [: the carrier of (L), the carrier of (L):] is non empty set
(L,(L,a)) is Element of the carrier of (L)
(L,X) is Element of the carrier of L
f . X is set
D is non empty set
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
[:(bool D),D:] is non empty set
bool [:(bool D),D:] is non empty set
f is Relation-like bool D -defined D -valued Function-like V18( bool D,D) Element of bool [:(bool D),D:]