:: YELLOW_0 semantic presentation

K95() is set
K99() is non empty non trivial V32() V33() V34() non finite cardinal limit_cardinal Element of bool K95()
bool K95() is set
K94() is non empty non trivial V32() V33() V34() non finite cardinal limit_cardinal set
bool K94() is non trivial non finite set
bool K99() is non trivial non finite set
2 is non empty V32() V33() V34() V38() finite cardinal Element of K99()
[:2,2:] is finite set
[:[:2,2:],2:] is finite set
bool [:[:2,2:],2:] is finite V44() set
{} is empty V32() V33() V34() V36() V37() V38() finite V44() cardinal {} -element set
1 is non empty V32() V33() V34() V38() finite cardinal Element of K99()
F₁() is non empty set
[:F₁(),F₁():] is set
bool [:F₁(),F₁():] is set
L is V1() V4(F₁()) V5(F₁()) Element of bool [:F₁(),F₁():]
RelStr(# F₁(),L #) is non empty strict RelStr
S is non empty strict RelStr
the carrier of S is non empty set
x is Element of the carrier of S
y is Element of the carrier of S
[x,y] is Element of [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
L is non empty RelStr
the carrier of L is non empty set
S is Element of the carrier of L
S is set
[S,S] is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
x is Element of the carrier of L
L is RelStr
the carrier of L is set
S is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
S is set
x is set
y is set
[S,x] is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
[x,y] is set
[S,y] is set
a is Element of the carrier of L
b is Element of the carrier of L
c9 is Element of the carrier of L
S is Element of the carrier of L
x is Element of the carrier of L
S is set
x is set
[S,x] is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
[x,S] is set
y is Element of the carrier of L
a is Element of the carrier of L
L is non empty RelStr
L is non empty trivial finite 1 -element V136() reflexive RelStr
the carrier of L is non empty trivial finite 1 -element set
the Element of the carrier of L is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x is set
y is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
L is set
{L} is non empty trivial finite 1 -element set
[:{L},{L}:] is finite set
bool [:{L},{L}:] is finite V44() set
S is V1() V4({L}) V5({L}) finite Element of bool [:{L},{L}:]
RelStr(# {L},S #) is non empty strict RelStr
the carrier of RelStr(# {L},S #) is non empty set
{{}} is non empty trivial finite V44() 1 -element set
[:{{}},{{}}:] is finite set
bool [:{{}},{{}}:] is finite V44() set
the V1() V4({{}}) V5({{}}) reflexive antisymmetric transitive V24({{}}) finite Element of bool [:{{}},{{}}:] is V1() V4({{}}) V5({{}}) reflexive antisymmetric transitive V24({{}}) finite Element of bool [:{{}},{{}}:]
RelStr(# {{}}, the V1() V4({{}}) V5({{}}) reflexive antisymmetric transitive V24({{}}) finite Element of bool [:{{}},{{}}:] #) is non empty trivial finite 1 -element strict V136() reflexive transitive antisymmetric with_suprema with_infima complete RelStr
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
S is RelStr
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of S
[a,b] is set
[x,y] is set
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
S is RelStr
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
x is set
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of S
b is Element of the carrier of S
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
S is RelStr
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
x is set
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of S
c9 is Element of the carrier of L
L is transitive RelStr
the carrier of L is set
S is Element of the carrier of L
x is Element of the carrier of L
y is set
a is Element of the carrier of L
a is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is set
S /\ the carrier of L is set
x is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
L is RelStr
the carrier of L is set
S is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
L is RelStr
the carrier of L is set
x is Element of the carrier of L
{x} is non empty trivial finite 1 -element set
S is Element of the carrier of L
y is Element of the carrier of L
y is Element of the carrier of L
L is RelStr
the carrier of L is set
x is Element of the carrier of L
y is Element of the carrier of L
{x,y} is non empty finite set
S is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
L is RelStr
the carrier of L is set
S is set
x is set
y is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
L is RelStr
the carrier of L is set
S is set
x is set
S \/ x is set
y is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
L is transitive RelStr
the carrier of L is set
S is set
x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
L is transitive RelStr
the carrier of L is set
S is set
x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
L is non empty RelStr
[#] L is non empty non proper Element of bool the carrier of L
the carrier of L is non empty set
bool the carrier of L is set
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
S is RelStr
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
x is Element of the carrier of L
y is Element of the carrier of S
x is Element of the carrier of L
y is Element of the carrier of S
L is non empty RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
b is Element of the carrier of L
c9 is Element of the carrier of L
a is Element of the carrier of L
L is RelStr
L is RelStr
the non empty V136() reflexive transitive antisymmetric with_suprema with_infima complete () () () RelStr is non empty V136() reflexive transitive antisymmetric with_suprema with_infima complete () () () RelStr
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
S is RelStr
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
x is set
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of S
c9 is Element of the carrier of L
b is Element of the carrier of S
c9 is Element of the carrier of L
b is Element of the carrier of L
b9 is Element of the carrier of S
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of S
c9 is Element of the carrier of L
b is Element of the carrier of S
b is Element of the carrier of L
b9 is Element of the carrier of S
c9 is Element of the carrier of L
L is antisymmetric RelStr
the carrier of L is set
S is set
x is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
y is Element of the carrier of L
L is antisymmetric RelStr
the carrier of L is set
S is set
x is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
y is Element of the carrier of L
L is non empty antisymmetric with_suprema with_infima complete () () () RelStr
S is set
the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : b₁ is_<=_than S } is set
y is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
c9 is Element of the carrier of L
b is Element of the carrier of L
b is Element of the carrier of L
a is Element of the carrier of L
L is antisymmetric RelStr
the carrier of L is set
y is Element of the carrier of L
S is Element of the carrier of L
x is Element of the carrier of L
S "\/" x is Element of the carrier of L
{S,x} is non empty finite set
a is Element of the carrier of L
b is Element of the carrier of L
b is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a is Element of the carrier of L
L is antisymmetric RelStr
the carrier of L is set
y is Element of the carrier of L
S is Element of the carrier of L
x is Element of the carrier of L
S "/\" x is Element of the carrier of L
{S,x} is non empty finite set
a is Element of the carrier of L
b is Element of the carrier of L
b is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
a is Element of the carrier of L
L is antisymmetric RelStr
the carrier of L is set
S is Element of the carrier of L
x is Element of the carrier of L
{S,x} is non empty finite set
y is Element of the carrier of L
S is Element of the carrier of L
x is Element of the carrier of L
S "\/" x is Element of the carrier of L
{S,x} is non empty finite set
y is Element of the carrier of L
L is antisymmetric RelStr
the carrier of L is set
S is Element of the carrier of L
x is Element of the carrier of L
{S,x} is non empty finite set
y is Element of the carrier of L
S is Element of the carrier of L
x is Element of the carrier of L
S "/\" x is Element of the carrier of L
{S,x} is non empty finite set
y is Element of the carrier of L
L is non empty antisymmetric with_suprema RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
S "\/" x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
c9 is Element of the carrier of L
L is non empty antisymmetric with_infima RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
S "/\" x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
c9 is Element of the carrier of L
L is non empty V136() reflexive antisymmetric with_suprema RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
S "\/" x is Element of the carrier of L
y is Element of the carrier of L
L is non empty V136() reflexive antisymmetric with_infima RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
S "/\" x is Element of the carrier of L
y is Element of the carrier of L
L is RelStr
the carrier of L is set
S is set
x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
x is Element of the carrier of L
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
S is RelStr
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
x is set
(L,x) is Element of the carrier of L
(S,x) is Element of the carrier of S
y is Element of the carrier of S
a is Element of the carrier of S
b is Element of the carrier of L
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
S is RelStr
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
x is set
(L,x) is Element of the carrier of L
(S,x) is Element of the carrier of S
y is Element of the carrier of S
a is Element of the carrier of S
b is Element of the carrier of L
L is non empty V136() reflexive transitive antisymmetric with_suprema with_infima complete () () () RelStr
latt L is non empty strict Lattice-like complete LattStr
S is set
(L,S) is Element of the carrier of L
the carrier of L is non empty set
"\/" (S,(latt L)) is Element of the carrier of (latt L)
the carrier of (latt L) is non empty set
(L,S) is Element of the carrier of L
"/\" (S,(latt L)) is Element of the carrier of (latt L)
{ b₁ where b₁ is Element of the carrier of (latt L) : b₁ is_less_than S } is set
"\/" ( { b₁ where b₁ is Element of the carrier of (latt L) : b₁ is_less_than S } ,(latt L)) is Element of the carrier of (latt L)
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) reflexive antisymmetric transitive V24( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is non empty strict V136() reflexive transitive antisymmetric RelStr
LattPOSet (latt L) is non empty strict V136() reflexive transitive antisymmetric RelStr
K256((latt L)) is V1() V4( the carrier of (latt L)) V5( the carrier of (latt L)) reflexive antisymmetric transitive V24( the carrier of (latt L)) Element of bool [: the carrier of (latt L), the carrier of (latt L):]
[: the carrier of (latt L), the carrier of (latt L):] is set
bool [: the carrier of (latt L), the carrier of (latt L):] is set
RelStr(# the carrier of (latt L),K256((latt L)) #) is non empty strict V136() reflexive transitive antisymmetric RelStr
the carrier of (LattPOSet (latt L)) is non empty set
a is Element of the carrier of L
b is Element of the carrier of (LattPOSet (latt L))
% b is Element of the carrier of (latt L)
(% b) % is Element of the carrier of (LattPOSet (latt L))
("/\" (S,(latt L))) % is Element of the carrier of (LattPOSet (latt L))
y is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of (latt L)
a % is Element of the carrier of (LattPOSet (latt L))
b is Element of the carrier of L
x is Element of the carrier of (LattPOSet (latt L))
% x is Element of the carrier of (latt L)
(% x) % is Element of the carrier of (LattPOSet (latt L))
L is non empty Lattice-like complete LattStr
LattPOSet L is non empty strict V136() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
K256(L) is V1() V4( the carrier of L) V5( the carrier of L) reflexive antisymmetric transitive V24( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L,K256(L) #) is non empty strict V136() reflexive transitive antisymmetric RelStr
S is set
"\/" (S,L) is Element of the carrier of L
((LattPOSet L),S) is Element of the carrier of (LattPOSet L)
the carrier of (LattPOSet L) is non empty set
"/\" (S,L) is Element of the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ is_less_than S } is set
"\/" ( { b₁ where b₁ is Element of the carrier of L : b₁ is_less_than S } ,L) is Element of the carrier of L
((LattPOSet L),S) is Element of the carrier of (LattPOSet L)
x is Element of the carrier of (LattPOSet L)
% x is Element of the carrier of L
(% x) % is Element of the carrier of (LattPOSet L)
("\/" (S,L)) % is Element of the carrier of (LattPOSet L)
x is Element of the carrier of (LattPOSet L)
% x is Element of the carrier of L
(% x) % is Element of the carrier of (LattPOSet L)
("/\" (S,L)) % is Element of the carrier of (LattPOSet L)
L is antisymmetric RelStr
the carrier of L is set
S is Element of the carrier of L
x is set
(L,x) is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
L is antisymmetric RelStr
the carrier of L is set
S is Element of the carrier of L
x is set
(L,x) is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
L is non empty antisymmetric with_suprema with_infima complete () () () RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is set
(L,x) is Element of the carrier of L
y is Element of the carrier of L
L is non empty antisymmetric with_suprema with_infima complete () () () RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is set
(L,x) is Element of the carrier of L
y is Element of the carrier of L
L is RelStr
S is set
x is set
(L,S) is Element of the carrier of L
the carrier of L is set
(L,x) is Element of the carrier of L
y is Element of the carrier of L
L is RelStr
S is set
x is set
(L,x) is Element of the carrier of L
the carrier of L is set
(L,S) is Element of the carrier of L
y is Element of the carrier of L
L is transitive antisymmetric RelStr
S is set
x is set
S \/ x is set
(L,(S \/ x)) is Element of the carrier of L
the carrier of L is set
(L,S) is Element of the carrier of L
(L,x) is Element of the carrier of L
(L,S) "\/" (L,x) is Element of the carrier of L
c9 is Element of the carrier of L
L is transitive antisymmetric RelStr
S is set
x is set
S \/ x is set
(L,(S \/ x)) is Element of the carrier of L
the carrier of L is set
(L,S) is Element of the carrier of L
(L,x) is Element of the carrier of L
(L,S) "/\" (L,x) is Element of the carrier of L
c9 is Element of the carrier of L
L is RelStr
the carrier of L is set
bool the carrier of L is set
L is non empty V136() reflexive antisymmetric RelStr
the carrier of L is non empty set
S is Element of the carrier of L
{S} is non empty trivial finite 1 -element Element of bool the carrier of L
bool the carrier of L is set
x is Element of the carrier of L
x is Element of the carrier of L
L is non empty V136() reflexive antisymmetric RelStr
the carrier of L is non empty set
S is Element of the carrier of L
{S} is non empty trivial finite 1 -element Element of bool the carrier of L
bool the carrier of L is set
(L,{S}) is Element of the carrier of L
(L,{S}) is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
L is non empty V136() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
{S,x} is non empty finite Element of bool the carrier of L
bool the carrier of L is set
(L,{S,x}) is Element of the carrier of L
S "/\" x is Element of the carrier of L
y is Element of the carrier of L
L is non empty V136() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
{S,x} is non empty finite Element of bool the carrier of L
bool the carrier of L is set
(L,{S,x}) is Element of the carrier of L
S "\/" x is Element of the carrier of L
y is Element of the carrier of L
L is non empty antisymmetric () RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
L is non empty antisymmetric () RelStr
the carrier of L is non empty set
S is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
x is Element of the carrier of L
L is RelStr
(L,{}) is Element of the carrier of L
the carrier of L is set
(L,{}) is Element of the carrier of L
L is non empty antisymmetric () RelStr
the carrier of L is non empty set
(L) is Element of the carrier of L
(L,{}) is Element of the carrier of L
S is Element of the carrier of L
L is non empty antisymmetric () RelStr
the carrier of L is non empty set
(L) is Element of the carrier of L
(L,{}) is Element of the carrier of L
S is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is set
x is set
y is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is set
x is set
(L,S) is Element of the carrier of L
(L,x) is Element of the carrier of L
y is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is set
x is set
y is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is set
x is set
(L,S) is Element of the carrier of L
(L,x) is Element of the carrier of L
y is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is set
S /\ the carrier of L is set
y is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of L
c9 is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is set
S /\ the carrier of L is set
(L,S) is Element of the carrier of L
(L,(S /\ the carrier of L)) is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is set
S /\ the carrier of L is set
(L,S) is Element of the carrier of L
(L,(S /\ the carrier of L)) is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is set
S is set
(L,S) is Element of the carrier of L
S /\ the carrier of L is set
x is Element of bool the carrier of L
y is Element of the carrier of L
L is non empty V136() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
bool the carrier of L is set
S is non empty finite Element of bool the carrier of L
x is set
y is set
{x} is non empty trivial finite 1 -element set
y \/ {x} is non empty set
a is Element of the carrier of L
{a} is non empty trivial finite 1 -element Element of bool the carrier of L
(L,y) is Element of the carrier of L
a is Element of the carrier of L
(L,y) "\/" a is Element of the carrier of L
b is Element of the carrier of L
{(L,y),a} is non empty finite Element of bool the carrier of L
c9 is Element of the carrier of L
c9 is Element of the carrier of L
S is Element of the carrier of L
x is Element of the carrier of L
{S,x} is non empty finite Element of bool the carrier of L
L is non empty V136() reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
bool the carrier of L is set
S is non empty finite Element of bool the carrier of L
x is set
y is set
{x} is non empty trivial finite 1 -element set
y \/ {x} is non empty set
a is Element of the carrier of L
{a} is non empty trivial finite 1 -element Element of bool the carrier of L
(L,y) is Element of the carrier of L
a is Element of the carrier of L
(L,y) "/\" a is Element of the carrier of L
b is Element of the carrier of L
{(L,y),a} is non empty finite Element of bool the carrier of L
c9 is Element of the carrier of L
c9 is Element of the carrier of L
S is Element of the carrier of L
x is Element of the carrier of L
{S,x} is non empty finite Element of bool the carrier of L
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
L is RelStr
L is RelStr
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
x is (L)
the InternalRel of x is V1() V4( the carrier of x) V5( the carrier of x) Element of bool [: the carrier of x, the carrier of x:]
the carrier of x is set
[: the carrier of x, the carrier of x:] is set
bool [: the carrier of x, the carrier of x:] is set
the InternalRel of L |_2 the carrier of x is V1() V4( the carrier of x) V5( the carrier of x) Element of bool [: the carrier of x, the carrier of x:]
the InternalRel of L /\ [: the carrier of x, the carrier of x:] is set
L is non empty RelStr
the carrier of L is non empty set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is non empty strict RelStr
x is (L)
the carrier of x is set
the InternalRel of x is V1() V4( the carrier of x) V5( the carrier of x) Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is set
bool [: the carrier of x, the carrier of x:] is set
the InternalRel of L |_2 the carrier of x is V1() V4( the carrier of x) V5( the carrier of x) Element of bool [: the carrier of x, the carrier of x:]
the InternalRel of L /\ [: the carrier of x, the carrier of x:] is set
L is RelStr
the carrier of L is set
bool the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
S is Element of bool the carrier of L
the InternalRel of L |_2 S is V1() V4(S) V5(S) Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is set
the InternalRel of L /\ [:S,S:] is set
RelStr(# S,( the InternalRel of L |_2 S) #) is strict RelStr
the InternalRel of RelStr(# S,( the InternalRel of L |_2 S) #) is V1() V4( the carrier of RelStr(# S,( the InternalRel of L |_2 S) #)) V5( the carrier of RelStr(# S,( the InternalRel of L |_2 S) #)) Element of bool [: the carrier of RelStr(# S,( the InternalRel of L |_2 S) #), the carrier of RelStr(# S,( the InternalRel of L |_2 S) #):]
the carrier of RelStr(# S,( the InternalRel of L |_2 S) #) is set
[: the carrier of RelStr(# S,( the InternalRel of L |_2 S) #), the carrier of RelStr(# S,( the InternalRel of L |_2 S) #):] is set
bool [: the carrier of RelStr(# S,( the InternalRel of L |_2 S) #), the carrier of RelStr(# S,( the InternalRel of L |_2 S) #):] is set
y is (L)
L is RelStr
S is (L) (L)
the carrier of S is set
x is (L) (L)
the carrier of x is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the InternalRel of x is V1() V4( the carrier of x) V5( the carrier of x) Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is set
bool [: the carrier of x, the carrier of x:] is set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
the carrier of L is set
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
the InternalRel of L |_2 the carrier of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
the InternalRel of L /\ [: the carrier of S, the carrier of S:] is set
L is RelStr
the carrier of L is set
bool the carrier of L is set
S is Element of bool the carrier of L
x is strict (L) (L)
the carrier of x is set
y is strict (L) (L)
the carrier of y is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
the InternalRel of L |_2 S is V1() V4(S) V5(S) Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is set
the InternalRel of L /\ [:S,S:] is set
RelStr(# S,( the InternalRel of L |_2 S) #) is strict RelStr
L is non empty RelStr
the carrier of L is non empty set
S is non empty (L)
the carrier of S is non empty set
x is Element of the carrier of S
L is RelStr
the carrier of L is set
S is (L)
the carrier of S is set
x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of S
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
[a,b] is set
[x,y] is set
L is RelStr
the carrier of L is set
S is (L) (L)
the carrier of S is set
x is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of S
[x,y] is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
the InternalRel of L |_2 the carrier of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
the InternalRel of L /\ [: the carrier of S, the carrier of S:] is set
[a,b] is set
L is non empty RelStr
the carrier of L is non empty set
S is non empty (L) (L)
the carrier of S is non empty set
x is set
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of S
c9 is Element of the carrier of L
b is Element of the carrier of S
c9 is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
S is non empty (L)
the carrier of S is non empty set
bool the carrier of S is set
x is Element of bool the carrier of S
y is Element of the carrier of L
a is Element of the carrier of S
b is Element of the carrier of L
c9 is Element of the carrier of S
b is Element of the carrier of L
c9 is Element of the carrier of S
L is V136() reflexive RelStr
S is (L) (L)
x is set
the carrier of S is set
[x,x] is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
the carrier of L is set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) reflexive V24( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
the InternalRel of L |_2 the carrier of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
the InternalRel of L /\ [: the carrier of S, the carrier of S:] is set
L is transitive RelStr
S is (L) (L)
the carrier of S is set
x is Element of the carrier of S
y is Element of the carrier of S
a is Element of the carrier of S
the carrier of L is set
[y,a] is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
[x,y] is set
b is Element of the carrier of L
c9 is Element of the carrier of L
b is Element of the carrier of L
L is antisymmetric RelStr
S is (L) (L)
the carrier of S is set
x is Element of the carrier of S
y is Element of the carrier of S
the carrier of L is set
[x,y] is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is set
bool [: the carrier of S, the carrier of S:] is set
a is Element of the carrier of L
b is Element of the carrier of L
L is non empty RelStr
L is non empty RelStr
L is non empty RelStr
S is (L)
the carrier of S is set
bool the carrier of S is set
the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
{x,y} is non empty finite Element of bool the carrier of L
bool the carrier of L is set
(L,{x,y}) is Element of the carrier of L
S is (L)
the carrier of S is set
bool the carrier of S is set
the carrier of L is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
{x,y} is non empty finite Element of bool the carrier of L
bool the carrier of L is set
(L,{x,y}) is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
the InternalRel of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is set
bool [: the carrier of L, the carrier of L:] is set
the InternalRel of L |_2 the carrier of L is V1() V4( the carrier of L) V5( the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
the InternalRel of L /\ [: the carrier of L, the carrier of L:] is set
RelStr(# the carrier of L, the InternalRel of L #) is non empty strict RelStr
S is non empty strict (L) (L)
the carrier of S is non empty set
bool the carrier of S is set
x is Element of bool the carrier of S
(L,x) is Element of the carrier of L
the carrier of S is non empty set
bool the carrier of S is set
x is Element of bool the carrier of S
(L,x) is Element of the carrier of L
L is non empty transitive RelStr
S is non empty transitive (L) (L)
the carrier of S is non empty set
bool the carrier of S is set
x is Element of bool the carrier of S
(L,x) is Element of the carrier of L
the carrier of L is non empty set
(S,x) is Element of the carrier of S
y is Element of the carrier of S
a is Element of the carrier of S
b is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of S
b is Element of the carrier of S
c9 is Element of the carrier of L
b is Element of the carrier of L
L is non empty transitive RelStr
S is non empty transitive (L) (L)
the carrier of S is non empty set
bool the carrier of S is set
x is Element of bool the carrier of S
(L,x) is Element of the carrier of L
the carrier of L is non empty set
(S,x) is Element of the carrier of S
y is Element of the carrier of S
a is Element of the carrier of S
b is Element of the carrier of L
a is Element of the carrier of L
b is Element of the carrier of S
b is Element of the carrier of S
c9 is Element of the carrier of L
b is Element of the carrier of L
L is non empty transitive RelStr
S is non empty transitive (L) (L)
the carrier of S is non empty set
x is Element of the carrier of S
y is Element of the carrier of S
{x,y} is non empty finite Element of bool the carrier of S
bool the carrier of S is set
(L,{x,y}) is Element of the carrier of L
the carrier of L is non empty set
(S,{x,y}) is Element of the carrier of S
L is non empty transitive RelStr
S is non empty transitive (L) (L)
the carrier of S is non empty set
x is Element of the carrier of S
y is Element of the carrier of S
{x,y} is non empty finite Element of bool the carrier of S
bool the carrier of S is set
(L,{x,y}) is Element of the carrier of L
the carrier of L is non empty set
(S,{x,y}) is Element of the carrier of S
L is non empty transitive antisymmetric with_infima RelStr
S is non empty transitive antisymmetric (L) (L) (L)
the carrier of S is non empty set
the carrier of L is non empty set
x is Element of the carrier of S
y is Element of the carrier of S
a is Element of the carrier of L
b is Element of the carrier of L
{a,b} is non empty finite Element of bool the carrier of L
bool the carrier of L is set
(L,{a,b}) is Element of the carrier of L
{x,y} is non empty finite Element of bool the carrier of S
bool the carrier of S is set
L is non empty transitive antisymmetric with_suprema RelStr
S is non empty transitive antisymmetric (L) (L) (L)
the carrier of S is non empty set
the carrier of L is non empty set
x is Element of the carrier of S
y is Element of the carrier of S
a is Element of the carrier of L
b is Element of the carrier of L
{a,b} is non empty finite Element of bool the carrier of L
bool the carrier of L is set
(L,{a,b}) is Element of the carrier of L
{x,y} is non empty finite Element of bool the carrier of S
bool the carrier of S is set
L is non empty V136() reflexive transitive antisymmetric with_suprema with_infima complete () () () RelStr
S is non empty V136() reflexive transitive antisymmetric (L) (L)
the carrier of S is non empty set
bool the carrier of S is set
x is Element of bool the carrier of S
(L,x) is Element of the carrier of L
the carrier of L is non empty set
(S,x) is Element of the carrier of S
L is non empty V136() reflexive transitive antisymmetric with_suprema with_infima complete () () () RelStr
S is non empty V136() reflexive transitive antisymmetric (L) (L)
the carrier of S is non empty set
bool the carrier of S is set
x is Element of bool the carrier of S
(L,x) is Element of the carrier of L
the carrier of L is non empty set
(S,x) is Element of the carrier of S
L is non empty V136() reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
S is non empty V136() reflexive transitive antisymmetric with_infima (L) (L) (L)
the carrier of S is non empty set
x is Element of the carrier of S
y is Element of the carrier of S
x "/\" y is Element of the carrier of S
a is Element of the carrier of L
b is Element of the carrier of L
a "/\" b is Element of the carrier of L
{a,b} is non empty finite Element of bool the carrier of L
bool the carrier of L is set
{x,y} is non empty finite Element of bool the carrier of S
bool the carrier of S is set
(L,{x,y}) is Element of the carrier of L
(S,{x,y}) is Element of the carrier of S
(L,{a,b}) is Element of the carrier of L
L is non empty V136() reflexive transitive antisymmetric with_suprema RelStr
the carrier of L is non empty set
S is non empty V136() reflexive transitive antisymmetric with_suprema (L) (L) (L)
the carrier of S is non empty set
x is Element of the carrier of S
y is Element of the carrier of S
x "\/" y is Element of the carrier of S
a is Element of the carrier of L
b is Element of the carrier of L
a "\/" b is Element of the carrier of L
{a,b} is non empty finite Element of bool the carrier of L
bool the carrier of L is set
{x,y} is non empty finite Element of bool the carrier of S
bool the carrier of S is set
(L,{x,y}) is Element of the carrier of L
(S,{x,y}) is Element of the carrier of S
(L,{a,b}) is Element of the carrier of L