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

[:F

bool [:F

L is V1() V4(F

RelStr(# F

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

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

"\/" ( { b

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

"\/" ( { b

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