:: WAYBEL20 semantic presentation

K117() is Element of bool K113()

K113() is set

bool K113() is non empty set

K102() is set

bool K102() is non empty set

bool K117() is non empty set

K114() is set

K115() is set

K116() is set

[:K113(),K113():] is Relation-like set

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

K339() is non empty V75() L8()

the carrier of K339() is non empty set

K344() is non empty V75() V97() V98() V99() V101() V151() V152() V153() V154() V155() V156() L8()

K345() is non empty V75() V99() V101() V154() V155() V156() M15(K344())

K346() is non empty V75() V97() V99() V101() V154() V155() V156() V157() M18(K344(),K345())

K348() is non empty V75() V97() V99() V101() L8()

K349() is non empty V75() V97() V99() V101() V157() M15(K348())

{} is empty Relation-like non-empty empty-yielding finite finite-yielding V34() set

1 is non empty set

{{},1} is non empty finite set

proj1 {} is empty Relation-like non-empty empty-yielding finite finite-yielding V34() set

proj2 {} is empty Relation-like non-empty empty-yielding finite finite-yielding V34() set

L is set

id L is Relation-like L -defined L -valued V17(L) V25(L,L) reflexive symmetric antisymmetric transitive Element of bool [:L,L:]

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

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

bool (id L) is non empty set

p is Relation-like L -defined L -valued Element of bool (id L)

proj1 p is set

proj2 p is set

Lc is set

pc is set

[Lc,pc] is V1() set

{Lc,pc} is non empty finite set

{Lc} is non empty finite set

{{Lc,pc},{Lc}} is non empty finite V34() set

pc is set

[pc,Lc] is V1() set

{pc,Lc} is non empty finite set

{pc} is non empty finite set

{{pc,Lc},{pc}} is non empty finite V34() set

L is non empty set

p is non empty set

[:L,p:] is non empty Relation-like set

bool [:L,p:] is non empty set

[:L,L:] is non empty Relation-like set

[:p,p:] is non empty Relation-like set

id p is non empty Relation-like p -defined p -valued V17(p) V25(p,p) reflexive symmetric antisymmetric transitive Element of bool [:p,p:]

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

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

Lc is non empty Relation-like L -defined p -valued Function-like V17(L) V25(L,p) Element of bool [:L,p:]

[:Lc,Lc:] is non empty Relation-like [:L,L:] -defined [:p,p:] -valued Function-like V17([:L,L:]) V25([:L,L:],[:p,p:]) Element of bool [:[:L,L:],[:p,p:]:]

[:[:L,L:],[:p,p:]:] is non empty Relation-like set

bool [:[:L,L:],[:p,p:]:] is non empty set

[:Lc,Lc:] " (id p) is Relation-like L -defined L -valued Element of bool [:L,L:]

dom Lc is non empty Element of bool L

bool L is non empty set

dom [:Lc,Lc:] is non empty Relation-like L -defined L -valued Element of bool [:L,L:]

[:(dom Lc),(dom Lc):] is non empty Relation-like set

cpc is Relation-like L -defined L -valued Element of bool [:L,L:]

X9 is set

[X9,X9] is V1() set

{X9,X9} is non empty finite set

{X9} is non empty finite set

{{X9,X9},{X9}} is non empty finite V34() set

x is Element of L

Lc . x is Element of p

[(Lc . x),(Lc . x)] is V1() Element of [:p,p:]

{(Lc . x),(Lc . x)} is non empty finite set

{(Lc . x)} is non empty finite set

{{(Lc . x),(Lc . x)},{(Lc . x)}} is non empty finite V34() set

Lc . X9 is set

[(Lc . X9),(Lc . X9)] is V1() set

{(Lc . X9),(Lc . X9)} is non empty finite set

{(Lc . X9)} is non empty finite set

{{(Lc . X9),(Lc . X9)},{(Lc . X9)}} is non empty finite V34() set

[:Lc,Lc:] . (X9,X9) is set

[:Lc,Lc:] . [X9,X9] is set

dom cpc is Element of bool L

field cpc is set

X9 is set

x is set

[X9,x] is V1() set

{X9,x} is non empty finite set

{X9} is non empty finite set

{{X9,x},{X9}} is non empty finite V34() set

[x,X9] is V1() set

{x,X9} is non empty finite set

{x} is non empty finite set

{{x,X9},{x}} is non empty finite V34() set

Lc . x is set

Lc . X9 is set

[(Lc . x),(Lc . X9)] is V1() set

{(Lc . x),(Lc . X9)} is non empty finite set

{(Lc . x)} is non empty finite set

{{(Lc . x),(Lc . X9)},{(Lc . x)}} is non empty finite V34() set

[:Lc,Lc:] . (x,X9) is set

[:Lc,Lc:] . [x,X9] is set

[:Lc,Lc:] . [X9,x] is set

[(Lc . X9),(Lc . x)] is V1() set

{(Lc . X9),(Lc . x)} is non empty finite set

{(Lc . X9)} is non empty finite set

{{(Lc . X9),(Lc . x)},{(Lc . X9)}} is non empty finite V34() set

[:Lc,Lc:] . (X9,x) is set

x9 is Element of L

Lc . x9 is Element of p

y is Element of L

Lc . y is Element of p

X9 is set

x is set

x9 is set

[X9,x] is V1() set

{X9,x} is non empty finite set

{X9} is non empty finite set

{{X9,x},{X9}} is non empty finite V34() set

[x,x9] is V1() set

{x,x9} is non empty finite set

{x} is non empty finite set

{{x,x9},{x}} is non empty finite V34() set

[X9,x9] is V1() set

{X9,x9} is non empty finite set

{{X9,x9},{X9}} is non empty finite V34() set

Lc . X9 is set

Lc . x9 is set

[(Lc . X9),(Lc . x9)] is V1() set

{(Lc . X9),(Lc . x9)} is non empty finite set

{(Lc . X9)} is non empty finite set

{{(Lc . X9),(Lc . x9)},{(Lc . X9)}} is non empty finite V34() set

[:Lc,Lc:] . (X9,x9) is set

[:Lc,Lc:] . [X9,x9] is set

[:Lc,Lc:] . [x,x9] is set

Lc . x is set

[(Lc . x),(Lc . x9)] is V1() set

{(Lc . x),(Lc . x9)} is non empty finite set

{(Lc . x)} is non empty finite set

{{(Lc . x),(Lc . x9)},{(Lc . x)}} is non empty finite V34() set

[:Lc,Lc:] . (x,x9) is set

y is Element of L

Lc . y is Element of p

x is Element of L

Lc . x is Element of p

[:Lc,Lc:] . [X9,x] is set

[(Lc . X9),(Lc . x)] is V1() set

{(Lc . X9),(Lc . x)} is non empty finite set

{{(Lc . X9),(Lc . x)},{(Lc . X9)}} is non empty finite V34() set

[:Lc,Lc:] . (X9,x) is set

L is RelStr

the carrier of L is set

Lc is RelStr

the carrier of Lc is set

[: the carrier of L, the carrier of Lc:] is Relation-like set

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

p is RelStr

the carrier of p is set

pc is RelStr

the carrier of pc is set

[: the carrier of p, the carrier of pc:] is Relation-like set

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

cpc is Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

X9 is Relation-like the carrier of p -defined the carrier of pc -valued Function-like V25( the carrier of p, the carrier of pc) Element of bool [: the carrier of p, the carrier of pc:]

[:cpc,X9:] is Relation-like Function-like set

[:L,p:] is strict RelStr

the carrier of [:L,p:] is set

[:Lc,pc:] is strict RelStr

the carrier of [:Lc,pc:] is set

[: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is Relation-like set

bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty set

[: the carrier of L, the carrier of p:] is Relation-like set

[: the carrier of Lc, the carrier of pc:] is Relation-like set

[:cpc,X9:] is Relation-like [: the carrier of L, the carrier of p:] -defined [: the carrier of Lc, the carrier of pc:] -valued Function-like V25([: the carrier of L, the carrier of p:],[: the carrier of Lc, the carrier of pc:]) Element of bool [:[: the carrier of L, the carrier of p:],[: the carrier of Lc, the carrier of pc:]:]

[:[: the carrier of L, the carrier of p:],[: the carrier of Lc, the carrier of pc:]:] is Relation-like set

bool [:[: the carrier of L, the carrier of p:],[: the carrier of Lc, the carrier of pc:]:] is non empty set

L is Relation-like Function-like set

p is Relation-like Function-like set

[:L,p:] is Relation-like Function-like set

Lc is set

[:L,p:] .: Lc is set

proj1 ([:L,p:] .: Lc) is set

proj1 Lc is set

L .: (proj1 Lc) is set

proj2 ([:L,p:] .: Lc) is set

proj2 Lc is set

p .: (proj2 Lc) is set

proj1 [:L,p:] is set

proj1 L is set

proj1 p is set

[:(proj1 L),(proj1 p):] is Relation-like set

pc is set

cpc is set

[pc,cpc] is V1() set

{pc,cpc} is non empty finite set

{pc} is non empty finite set

{{pc,cpc},{pc}} is non empty finite V34() set

X9 is set

[:L,p:] . X9 is set

x is set

x9 is set

[x,x9] is V1() set

{x,x9} is non empty finite set

{x} is non empty finite set

{{x,x9},{x}} is non empty finite V34() set

[:L,p:] . (x,x9) is set

[:L,p:] . [x,x9] is set

L . x is set

p . x9 is set

[(L . x),(p . x9)] is V1() set

{(L . x),(p . x9)} is non empty finite set

{(L . x)} is non empty finite set

{{(L . x),(p . x9)},{(L . x)}} is non empty finite V34() set

pc is set

cpc is set

[cpc,pc] is V1() set

{cpc,pc} is non empty finite set

{cpc} is non empty finite set

{{cpc,pc},{cpc}} is non empty finite V34() set

X9 is set

[:L,p:] . X9 is set

x is set

x9 is set

[x,x9] is V1() set

{x,x9} is non empty finite set

{x} is non empty finite set

{{x,x9},{x}} is non empty finite V34() set

[:L,p:] . (x,x9) is set

[:L,p:] . [x,x9] is set

L . x is set

p . x9 is set

[(L . x),(p . x9)] is V1() set

{(L . x),(p . x9)} is non empty finite set

{(L . x)} is non empty finite set

{{(L . x),(p . x9)},{(L . x)}} is non empty finite V34() set

L is Relation-like Function-like set

proj1 L is set

p is Relation-like Function-like set

proj1 p is set

[:(proj1 L),(proj1 p):] is Relation-like set

[:L,p:] is Relation-like Function-like set

Lc is set

[:L,p:] .: Lc is set

proj1 ([:L,p:] .: Lc) is set

proj1 Lc is set

L .: (proj1 Lc) is set

proj2 ([:L,p:] .: Lc) is set

proj2 Lc is set

p .: (proj2 Lc) is set

proj1 [:L,p:] is set

pc is set

cpc is set

L . cpc is set

X9 is set

[cpc,X9] is V1() set

{cpc,X9} is non empty finite set

{cpc} is non empty finite set

{{cpc,X9},{cpc}} is non empty finite V34() set

[:L,p:] . (cpc,X9) is set

[:L,p:] . [cpc,X9] is set

p . X9 is set

[(L . cpc),(p . X9)] is V1() set

{(L . cpc),(p . X9)} is non empty finite set

{(L . cpc)} is non empty finite set

{{(L . cpc),(p . X9)},{(L . cpc)}} is non empty finite V34() set

[pc,(p . X9)] is V1() set

{pc,(p . X9)} is non empty finite set

{pc} is non empty finite set

{{pc,(p . X9)},{pc}} is non empty finite V34() set

pc is set

cpc is set

p . cpc is set

X9 is set

[X9,cpc] is V1() set

{X9,cpc} is non empty finite set

{X9} is non empty finite set

{{X9,cpc},{X9}} is non empty finite V34() set

[:L,p:] . (X9,cpc) is set

[:L,p:] . [X9,cpc] is set

L . X9 is set

[(L . X9),(p . cpc)] is V1() set

{(L . X9),(p . cpc)} is non empty finite set

{(L . X9)} is non empty finite set

{{(L . X9),(p . cpc)},{(L . X9)}} is non empty finite V34() set

[(L . X9),pc] is V1() set

{(L . X9),pc} is non empty finite set

{{(L . X9),pc},{(L . X9)}} is non empty finite V34() set

L is non empty antisymmetric RelStr

Top L is Element of the carrier of L

the carrier of L is non empty set

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

p is Element of the carrier of L

L is non empty antisymmetric RelStr

Bottom L is Element of the carrier of L

the carrier of L is non empty set

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

p is Element of the carrier of L

L is non empty antisymmetric RelStr

p is non empty antisymmetric RelStr

[:L,p:] is non empty strict antisymmetric RelStr

the carrier of [:L,p:] is non empty set

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

Lc is Element of bool the carrier of [:L,p:]

"/\" (Lc,[:L,p:]) is Element of the carrier of [:L,p:]

proj1 Lc is Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

"/\" ((proj1 Lc),L) is Element of the carrier of L

proj2 Lc is Element of bool the carrier of p

the carrier of p is non empty set

bool the carrier of p is non empty set

"/\" ((proj2 Lc),p) is Element of the carrier of p

[("/\" ((proj1 Lc),L)),("/\" ((proj2 Lc),p))] is V1() Element of the carrier of [:L,p:]

{("/\" ((proj1 Lc),L)),("/\" ((proj2 Lc),p))} is non empty finite set

{("/\" ((proj1 Lc),L))} is non empty finite set

{{("/\" ((proj1 Lc),L)),("/\" ((proj2 Lc),p))},{("/\" ((proj1 Lc),L))}} is non empty finite V34() set

L is non empty antisymmetric RelStr

p is non empty antisymmetric RelStr

[:L,p:] is non empty strict antisymmetric RelStr

the carrier of [:L,p:] is non empty set

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

Lc is Element of bool the carrier of [:L,p:]

"\/" (Lc,[:L,p:]) is Element of the carrier of [:L,p:]

proj1 Lc is Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

"\/" ((proj1 Lc),L) is Element of the carrier of L

proj2 Lc is Element of bool the carrier of p

the carrier of p is non empty set

bool the carrier of p is non empty set

"\/" ((proj2 Lc),p) is Element of the carrier of p

[("\/" ((proj1 Lc),L)),("\/" ((proj2 Lc),p))] is V1() Element of the carrier of [:L,p:]

{("\/" ((proj1 Lc),L)),("\/" ((proj2 Lc),p))} is non empty finite set

{("\/" ((proj1 Lc),L))} is non empty finite set

{{("\/" ((proj1 Lc),L)),("\/" ((proj2 Lc),p))},{("\/" ((proj1 Lc),L))}} is non empty finite V34() set

L is non empty antisymmetric RelStr

the carrier of L is non empty set

Lc is non empty antisymmetric RelStr

the carrier of Lc is non empty set

[: the carrier of L, the carrier of Lc:] is non empty Relation-like set

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

p is non empty antisymmetric RelStr

the carrier of p is non empty set

pc is non empty antisymmetric RelStr

the carrier of pc is non empty set

[: the carrier of p, the carrier of pc:] is non empty Relation-like set

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

[:L,p:] is non empty strict antisymmetric RelStr

[:Lc,pc:] is non empty strict antisymmetric RelStr

cpc is non empty Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

X9 is non empty Relation-like the carrier of p -defined the carrier of pc -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of pc) Element of bool [: the carrier of p, the carrier of pc:]

(L,p,Lc,pc,cpc,X9) is non empty Relation-like the carrier of [:L,p:] -defined the carrier of [:Lc,pc:] -valued Function-like V17( the carrier of [:L,p:]) V25( the carrier of [:L,p:], the carrier of [:Lc,pc:]) Element of bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:]

the carrier of [:L,p:] is non empty set

the carrier of [:Lc,pc:] is non empty set

[: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty Relation-like set

bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty set

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

x is Element of bool the carrier of [:L,p:]

proj1 x is Element of bool the carrier of L

bool the carrier of L is non empty set

proj2 x is Element of bool the carrier of p

bool the carrier of p is non empty set

(L,p,Lc,pc,cpc,X9) .: x is Element of bool the carrier of [:Lc,pc:]

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

dom cpc is non empty Element of bool the carrier of L

dom X9 is non empty Element of bool the carrier of p

"/\" (((L,p,Lc,pc,cpc,X9) .: x),[:Lc,pc:]) is Element of the carrier of [:Lc,pc:]

"/\" (x,[:L,p:]) is Element of the carrier of [:L,p:]

(L,p,Lc,pc,cpc,X9) . ("/\" (x,[:L,p:])) is Element of the carrier of [:Lc,pc:]

[: the carrier of L, the carrier of p:] is non empty Relation-like set

proj2 ((L,p,Lc,pc,cpc,X9) .: x) is Element of bool the carrier of pc

bool the carrier of pc is non empty set

X9 .: (proj2 x) is Element of bool the carrier of pc

proj1 ((L,p,Lc,pc,cpc,X9) .: x) is Element of bool the carrier of Lc

bool the carrier of Lc is non empty set

cpc .: (proj1 x) is Element of bool the carrier of Lc

"/\" ((cpc .: (proj1 x)),Lc) is Element of the carrier of Lc

"/\" ((X9 .: (proj2 x)),pc) is Element of the carrier of pc

[("/\" ((cpc .: (proj1 x)),Lc)),("/\" ((X9 .: (proj2 x)),pc))] is V1() Element of the carrier of [:Lc,pc:]

{("/\" ((cpc .: (proj1 x)),Lc)),("/\" ((X9 .: (proj2 x)),pc))} is non empty finite set

{("/\" ((cpc .: (proj1 x)),Lc))} is non empty finite set

{{("/\" ((cpc .: (proj1 x)),Lc)),("/\" ((X9 .: (proj2 x)),pc))},{("/\" ((cpc .: (proj1 x)),Lc))}} is non empty finite V34() set

"/\" ((proj1 x),L) is Element of the carrier of L

cpc . ("/\" ((proj1 x),L)) is Element of the carrier of Lc

[(cpc . ("/\" ((proj1 x),L))),("/\" ((X9 .: (proj2 x)),pc))] is V1() Element of the carrier of [:Lc,pc:]

{(cpc . ("/\" ((proj1 x),L))),("/\" ((X9 .: (proj2 x)),pc))} is non empty finite set

{(cpc . ("/\" ((proj1 x),L)))} is non empty finite set

{{(cpc . ("/\" ((proj1 x),L))),("/\" ((X9 .: (proj2 x)),pc))},{(cpc . ("/\" ((proj1 x),L)))}} is non empty finite V34() set

"/\" ((proj2 x),p) is Element of the carrier of p

X9 . ("/\" ((proj2 x),p)) is Element of the carrier of pc

[(cpc . ("/\" ((proj1 x),L))),(X9 . ("/\" ((proj2 x),p)))] is V1() Element of the carrier of [:Lc,pc:]

{(cpc . ("/\" ((proj1 x),L))),(X9 . ("/\" ((proj2 x),p)))} is non empty finite set

{{(cpc . ("/\" ((proj1 x),L))),(X9 . ("/\" ((proj2 x),p)))},{(cpc . ("/\" ((proj1 x),L)))}} is non empty finite V34() set

(L,p,Lc,pc,cpc,X9) . (("/\" ((proj1 x),L)),("/\" ((proj2 x),p))) is set

[("/\" ((proj1 x),L)),("/\" ((proj2 x),p))] is V1() set

{("/\" ((proj1 x),L)),("/\" ((proj2 x),p))} is non empty finite set

{("/\" ((proj1 x),L))} is non empty finite set

{{("/\" ((proj1 x),L)),("/\" ((proj2 x),p))},{("/\" ((proj1 x),L))}} is non empty finite V34() set

(L,p,Lc,pc,cpc,X9) . [("/\" ((proj1 x),L)),("/\" ((proj2 x),p))] is set

L is non empty reflexive antisymmetric non void RelStr

the carrier of L is non empty set

Lc is non empty reflexive antisymmetric non void RelStr

the carrier of Lc is non empty set

[: the carrier of L, the carrier of Lc:] is non empty Relation-like set

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

p is non empty reflexive antisymmetric non void RelStr

the carrier of p is non empty set

pc is non empty reflexive antisymmetric non void RelStr

the carrier of pc is non empty set

[: the carrier of p, the carrier of pc:] is non empty Relation-like set

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

[:L,p:] is non empty strict reflexive antisymmetric non void RelStr

[:Lc,pc:] is non empty strict reflexive antisymmetric non void RelStr

cpc is non empty Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

X9 is non empty Relation-like the carrier of p -defined the carrier of pc -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of pc) Element of bool [: the carrier of p, the carrier of pc:]

(L,p,Lc,pc,cpc,X9) is non empty Relation-like the carrier of [:L,p:] -defined the carrier of [:Lc,pc:] -valued Function-like V17( the carrier of [:L,p:]) V25( the carrier of [:L,p:], the carrier of [:Lc,pc:]) Element of bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:]

the carrier of [:L,p:] is non empty set

the carrier of [:Lc,pc:] is non empty set

[: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty Relation-like set

bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty set

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

x is Element of bool the carrier of [:L,p:]

proj1 x is Element of bool the carrier of L

bool the carrier of L is non empty set

proj2 x is Element of bool the carrier of p

bool the carrier of p is non empty set

(L,p,Lc,pc,cpc,X9) .: x is Element of bool the carrier of [:Lc,pc:]

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

dom cpc is non empty Element of bool the carrier of L

dom X9 is non empty Element of bool the carrier of p

"/\" (((L,p,Lc,pc,cpc,X9) .: x),[:Lc,pc:]) is Element of the carrier of [:Lc,pc:]

"/\" (x,[:L,p:]) is Element of the carrier of [:L,p:]

(L,p,Lc,pc,cpc,X9) . ("/\" (x,[:L,p:])) is Element of the carrier of [:Lc,pc:]

[: the carrier of L, the carrier of p:] is non empty Relation-like set

proj2 ((L,p,Lc,pc,cpc,X9) .: x) is Element of bool the carrier of pc

bool the carrier of pc is non empty set

X9 .: (proj2 x) is Element of bool the carrier of pc

proj1 ((L,p,Lc,pc,cpc,X9) .: x) is Element of bool the carrier of Lc

bool the carrier of Lc is non empty set

cpc .: (proj1 x) is Element of bool the carrier of Lc

"/\" ((cpc .: (proj1 x)),Lc) is Element of the carrier of Lc

"/\" ((X9 .: (proj2 x)),pc) is Element of the carrier of pc

[("/\" ((cpc .: (proj1 x)),Lc)),("/\" ((X9 .: (proj2 x)),pc))] is V1() Element of the carrier of [:Lc,pc:]

{("/\" ((cpc .: (proj1 x)),Lc)),("/\" ((X9 .: (proj2 x)),pc))} is non empty finite set

{("/\" ((cpc .: (proj1 x)),Lc))} is non empty finite set

{{("/\" ((cpc .: (proj1 x)),Lc)),("/\" ((X9 .: (proj2 x)),pc))},{("/\" ((cpc .: (proj1 x)),Lc))}} is non empty finite V34() set

"/\" ((proj1 x),L) is Element of the carrier of L

cpc . ("/\" ((proj1 x),L)) is Element of the carrier of Lc

[(cpc . ("/\" ((proj1 x),L))),("/\" ((X9 .: (proj2 x)),pc))] is V1() Element of the carrier of [:Lc,pc:]

{(cpc . ("/\" ((proj1 x),L))),("/\" ((X9 .: (proj2 x)),pc))} is non empty finite set

{(cpc . ("/\" ((proj1 x),L)))} is non empty finite set

{{(cpc . ("/\" ((proj1 x),L))),("/\" ((X9 .: (proj2 x)),pc))},{(cpc . ("/\" ((proj1 x),L)))}} is non empty finite V34() set

"/\" ((proj2 x),p) is Element of the carrier of p

X9 . ("/\" ((proj2 x),p)) is Element of the carrier of pc

[(cpc . ("/\" ((proj1 x),L))),(X9 . ("/\" ((proj2 x),p)))] is V1() Element of the carrier of [:Lc,pc:]

{(cpc . ("/\" ((proj1 x),L))),(X9 . ("/\" ((proj2 x),p)))} is non empty finite set

{{(cpc . ("/\" ((proj1 x),L))),(X9 . ("/\" ((proj2 x),p)))},{(cpc . ("/\" ((proj1 x),L)))}} is non empty finite V34() set

(L,p,Lc,pc,cpc,X9) . (("/\" ((proj1 x),L)),("/\" ((proj2 x),p))) is set

[("/\" ((proj1 x),L)),("/\" ((proj2 x),p))] is V1() set

{("/\" ((proj1 x),L)),("/\" ((proj2 x),p))} is non empty finite set

{("/\" ((proj1 x),L))} is non empty finite set

{{("/\" ((proj1 x),L)),("/\" ((proj2 x),p))},{("/\" ((proj1 x),L))}} is non empty finite V34() set

(L,p,Lc,pc,cpc,X9) . [("/\" ((proj1 x),L)),("/\" ((proj2 x),p))] is set

L is non empty antisymmetric RelStr

the carrier of L is non empty set

Lc is non empty antisymmetric RelStr

the carrier of Lc is non empty set

[: the carrier of L, the carrier of Lc:] is non empty Relation-like set

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

p is non empty antisymmetric RelStr

the carrier of p is non empty set

pc is non empty antisymmetric RelStr

the carrier of pc is non empty set

[: the carrier of p, the carrier of pc:] is non empty Relation-like set

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

[:L,p:] is non empty strict antisymmetric RelStr

[:Lc,pc:] is non empty strict antisymmetric RelStr

cpc is non empty Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

X9 is non empty Relation-like the carrier of p -defined the carrier of pc -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of pc) Element of bool [: the carrier of p, the carrier of pc:]

(L,p,Lc,pc,cpc,X9) is non empty Relation-like the carrier of [:L,p:] -defined the carrier of [:Lc,pc:] -valued Function-like V17( the carrier of [:L,p:]) V25( the carrier of [:L,p:], the carrier of [:Lc,pc:]) Element of bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:]

the carrier of [:L,p:] is non empty set

the carrier of [:Lc,pc:] is non empty set

[: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty Relation-like set

bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty set

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

x is Element of bool the carrier of [:L,p:]

proj1 x is Element of bool the carrier of L

bool the carrier of L is non empty set

proj2 x is Element of bool the carrier of p

bool the carrier of p is non empty set

(L,p,Lc,pc,cpc,X9) .: x is Element of bool the carrier of [:Lc,pc:]

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

dom cpc is non empty Element of bool the carrier of L

dom X9 is non empty Element of bool the carrier of p

"\/" (((L,p,Lc,pc,cpc,X9) .: x),[:Lc,pc:]) is Element of the carrier of [:Lc,pc:]

"\/" (x,[:L,p:]) is Element of the carrier of [:L,p:]

(L,p,Lc,pc,cpc,X9) . ("\/" (x,[:L,p:])) is Element of the carrier of [:Lc,pc:]

[: the carrier of L, the carrier of p:] is non empty Relation-like set

proj2 ((L,p,Lc,pc,cpc,X9) .: x) is Element of bool the carrier of pc

bool the carrier of pc is non empty set

X9 .: (proj2 x) is Element of bool the carrier of pc

proj1 ((L,p,Lc,pc,cpc,X9) .: x) is Element of bool the carrier of Lc

bool the carrier of Lc is non empty set

cpc .: (proj1 x) is Element of bool the carrier of Lc

"\/" ((cpc .: (proj1 x)),Lc) is Element of the carrier of Lc

"\/" ((X9 .: (proj2 x)),pc) is Element of the carrier of pc

[("\/" ((cpc .: (proj1 x)),Lc)),("\/" ((X9 .: (proj2 x)),pc))] is V1() Element of the carrier of [:Lc,pc:]

{("\/" ((cpc .: (proj1 x)),Lc)),("\/" ((X9 .: (proj2 x)),pc))} is non empty finite set

{("\/" ((cpc .: (proj1 x)),Lc))} is non empty finite set

{{("\/" ((cpc .: (proj1 x)),Lc)),("\/" ((X9 .: (proj2 x)),pc))},{("\/" ((cpc .: (proj1 x)),Lc))}} is non empty finite V34() set

"\/" ((proj1 x),L) is Element of the carrier of L

cpc . ("\/" ((proj1 x),L)) is Element of the carrier of Lc

[(cpc . ("\/" ((proj1 x),L))),("\/" ((X9 .: (proj2 x)),pc))] is V1() Element of the carrier of [:Lc,pc:]

{(cpc . ("\/" ((proj1 x),L))),("\/" ((X9 .: (proj2 x)),pc))} is non empty finite set

{(cpc . ("\/" ((proj1 x),L)))} is non empty finite set

{{(cpc . ("\/" ((proj1 x),L))),("\/" ((X9 .: (proj2 x)),pc))},{(cpc . ("\/" ((proj1 x),L)))}} is non empty finite V34() set

"\/" ((proj2 x),p) is Element of the carrier of p

X9 . ("\/" ((proj2 x),p)) is Element of the carrier of pc

[(cpc . ("\/" ((proj1 x),L))),(X9 . ("\/" ((proj2 x),p)))] is V1() Element of the carrier of [:Lc,pc:]

{(cpc . ("\/" ((proj1 x),L))),(X9 . ("\/" ((proj2 x),p)))} is non empty finite set

{{(cpc . ("\/" ((proj1 x),L))),(X9 . ("\/" ((proj2 x),p)))},{(cpc . ("\/" ((proj1 x),L)))}} is non empty finite V34() set

(L,p,Lc,pc,cpc,X9) . (("\/" ((proj1 x),L)),("\/" ((proj2 x),p))) is set

[("\/" ((proj1 x),L)),("\/" ((proj2 x),p))] is V1() set

{("\/" ((proj1 x),L)),("\/" ((proj2 x),p))} is non empty finite set

{("\/" ((proj1 x),L))} is non empty finite set

{{("\/" ((proj1 x),L)),("\/" ((proj2 x),p))},{("\/" ((proj1 x),L))}} is non empty finite V34() set

(L,p,Lc,pc,cpc,X9) . [("\/" ((proj1 x),L)),("\/" ((proj2 x),p))] is set

L is non empty reflexive antisymmetric non void RelStr

the carrier of L is non empty set

Lc is non empty reflexive antisymmetric non void RelStr

the carrier of Lc is non empty set

[: the carrier of L, the carrier of Lc:] is non empty Relation-like set

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

p is non empty reflexive antisymmetric non void RelStr

the carrier of p is non empty set

pc is non empty reflexive antisymmetric non void RelStr

the carrier of pc is non empty set

[: the carrier of p, the carrier of pc:] is non empty Relation-like set

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

[:L,p:] is non empty strict reflexive antisymmetric non void RelStr

[:Lc,pc:] is non empty strict reflexive antisymmetric non void RelStr

cpc is non empty Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

X9 is non empty Relation-like the carrier of p -defined the carrier of pc -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of pc) Element of bool [: the carrier of p, the carrier of pc:]

(L,p,Lc,pc,cpc,X9) is non empty Relation-like the carrier of [:L,p:] -defined the carrier of [:Lc,pc:] -valued Function-like V17( the carrier of [:L,p:]) V25( the carrier of [:L,p:], the carrier of [:Lc,pc:]) Element of bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:]

the carrier of [:L,p:] is non empty set

the carrier of [:Lc,pc:] is non empty set

[: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty Relation-like set

bool [: the carrier of [:L,p:], the carrier of [:Lc,pc:]:] is non empty set

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

x is Element of bool the carrier of [:L,p:]

proj1 x is Element of bool the carrier of L

bool the carrier of L is non empty set

proj2 x is Element of bool the carrier of p

bool the carrier of p is non empty set

(L,p,Lc,pc,cpc,X9) .: x is Element of bool the carrier of [:Lc,pc:]

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

dom cpc is non empty Element of bool the carrier of L

dom X9 is non empty Element of bool the carrier of p

"\/" (((L,p,Lc,pc,cpc,X9) .: x),[:Lc,pc:]) is Element of the carrier of [:Lc,pc:]

"\/" (x,[:L,p:]) is Element of the carrier of [:L,p:]

(L,p,Lc,pc,cpc,X9) . ("\/" (x,[:L,p:])) is Element of the carrier of [:Lc,pc:]

[: the carrier of L, the carrier of p:] is non empty Relation-like set

proj2 ((L,p,Lc,pc,cpc,X9) .: x) is Element of bool the carrier of pc

bool the carrier of pc is non empty set

X9 .: (proj2 x) is Element of bool the carrier of pc

proj1 ((L,p,Lc,pc,cpc,X9) .: x) is Element of bool the carrier of Lc

bool the carrier of Lc is non empty set

cpc .: (proj1 x) is Element of bool the carrier of Lc

"\/" ((cpc .: (proj1 x)),Lc) is Element of the carrier of Lc

"\/" ((X9 .: (proj2 x)),pc) is Element of the carrier of pc

[("\/" ((cpc .: (proj1 x)),Lc)),("\/" ((X9 .: (proj2 x)),pc))] is V1() Element of the carrier of [:Lc,pc:]

{("\/" ((cpc .: (proj1 x)),Lc)),("\/" ((X9 .: (proj2 x)),pc))} is non empty finite set

{("\/" ((cpc .: (proj1 x)),Lc))} is non empty finite set

{{("\/" ((cpc .: (proj1 x)),Lc)),("\/" ((X9 .: (proj2 x)),pc))},{("\/" ((cpc .: (proj1 x)),Lc))}} is non empty finite V34() set

"\/" ((proj1 x),L) is Element of the carrier of L

cpc . ("\/" ((proj1 x),L)) is Element of the carrier of Lc

[(cpc . ("\/" ((proj1 x),L))),("\/" ((X9 .: (proj2 x)),pc))] is V1() Element of the carrier of [:Lc,pc:]

{(cpc . ("\/" ((proj1 x),L))),("\/" ((X9 .: (proj2 x)),pc))} is non empty finite set

{(cpc . ("\/" ((proj1 x),L)))} is non empty finite set

{{(cpc . ("\/" ((proj1 x),L))),("\/" ((X9 .: (proj2 x)),pc))},{(cpc . ("\/" ((proj1 x),L)))}} is non empty finite V34() set

"\/" ((proj2 x),p) is Element of the carrier of p

X9 . ("\/" ((proj2 x),p)) is Element of the carrier of pc

[(cpc . ("\/" ((proj1 x),L))),(X9 . ("\/" ((proj2 x),p)))] is V1() Element of the carrier of [:Lc,pc:]

{(cpc . ("\/" ((proj1 x),L))),(X9 . ("\/" ((proj2 x),p)))} is non empty finite set

{{(cpc . ("\/" ((proj1 x),L))),(X9 . ("\/" ((proj2 x),p)))},{(cpc . ("\/" ((proj1 x),L)))}} is non empty finite V34() set

(L,p,Lc,pc,cpc,X9) . (("\/" ((proj1 x),L)),("\/" ((proj2 x),p))) is set

[("\/" ((proj1 x),L)),("\/" ((proj2 x),p))] is V1() set

{("\/" ((proj1 x),L)),("\/" ((proj2 x),p))} is non empty finite set

{("\/" ((proj1 x),L))} is non empty finite set

{{("\/" ((proj1 x),L)),("\/" ((proj2 x),p))},{("\/" ((proj1 x),L))}} is non empty finite V34() set

(L,p,Lc,pc,cpc,X9) . [("\/" ((proj1 x),L)),("\/" ((proj2 x),p))] is set

L is non empty antisymmetric RelStr

[:L,L:] is non empty strict antisymmetric RelStr

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

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

the carrier of L is non empty set

id the carrier of L is non empty Relation-like the carrier of L -defined the carrier of L -valued V17( the carrier of L) V25( the carrier of L, the carrier of L) reflexive symmetric antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

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

p is Element of bool the carrier of [:L,L:]

"/\" (p,[:L,L:]) is Element of the carrier of [:L,L:]

proj1 p is Element of bool the carrier of L

bool the carrier of L is non empty set

"/\" ((proj1 p),L) is Element of the carrier of L

proj2 p is Element of bool the carrier of L

"/\" ((proj2 p),L) is Element of the carrier of L

[("/\" ((proj1 p),L)),("/\" ((proj2 p),L))] is V1() Element of the carrier of [:L,L:]

{("/\" ((proj1 p),L)),("/\" ((proj2 p),L))} is non empty finite set

{("/\" ((proj1 p),L))} is non empty finite set

{{("/\" ((proj1 p),L)),("/\" ((proj2 p),L))},{("/\" ((proj1 p),L))}} is non empty finite V34() set

L is non empty antisymmetric RelStr

[:L,L:] is non empty strict antisymmetric RelStr

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

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

the carrier of L is non empty set

id the carrier of L is non empty Relation-like the carrier of L -defined the carrier of L -valued V17( the carrier of L) V25( the carrier of L, the carrier of L) reflexive symmetric antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]

[: the carrier of L, the carrier of L:] is non empty Relation-like set

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

p is Element of bool the carrier of [:L,L:]

"\/" (p,[:L,L:]) is Element of the carrier of [:L,L:]

proj1 p is Element of bool the carrier of L

bool the carrier of L is non empty set

"\/" ((proj1 p),L) is Element of the carrier of L

proj2 p is Element of bool the carrier of L

"\/" ((proj2 p),L) is Element of the carrier of L

[("\/" ((proj1 p),L)),("\/" ((proj2 p),L))] is V1() Element of the carrier of [:L,L:]

{("\/" ((proj1 p),L)),("\/" ((proj2 p),L))} is non empty finite set

{("\/" ((proj1 p),L))} is non empty finite set

{{("\/" ((proj1 p),L)),("\/" ((proj2 p),L))},{("\/" ((proj1 p),L))}} is non empty finite V34() set

L is non empty RelStr

p is non empty RelStr

the carrier of p is non empty set

Lc is Element of the carrier of p

the carrier of L is non empty set

[: the carrier of p, the carrier of L:] is non empty Relation-like set

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

pc is non empty Relation-like the carrier of p -defined the carrier of L -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of L) Element of bool [: the carrier of p, the carrier of L:]

pc . Lc is Element of the carrier of L

cpc is Element of the carrier of L

L is non empty RelStr

p is non empty RelStr

the carrier of p is non empty set

the carrier of L is non empty set

[: the carrier of p, the carrier of L:] is non empty Relation-like set

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

Lc is non empty Relation-like the carrier of p -defined the carrier of L -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of L) Element of bool [: the carrier of p, the carrier of L:]

pc is Element of the carrier of p

cpc is Element of the carrier of p

X9 is Element of the carrier of p

Lc . X9 is Element of the carrier of L

Lc . cpc is Element of the carrier of L

Lc . pc is Element of the carrier of L

y is Element of the carrier of L

x9 is Element of the carrier of L

x is Element of the carrier of L

L is non empty RelStr

p is non empty RelStr

the carrier of p is non empty set

the carrier of L is non empty set

[: the carrier of p, the carrier of L:] is non empty Relation-like set

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

Lc is non empty Relation-like the carrier of p -defined the carrier of L -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of L) Element of bool [: the carrier of p, the carrier of L:]

pc is Element of the carrier of p

cpc is Element of the carrier of p

Lc . cpc is Element of the carrier of L

Lc . pc is Element of the carrier of L

x is Element of the carrier of L

X9 is Element of the carrier of L

dom Lc is non empty Element of bool the carrier of p

bool the carrier of p is non empty set

L is non empty RelStr

p is non empty RelStr

the carrier of p is non empty set

bool the carrier of p is non empty set

Lc is Element of bool the carrier of p

the carrier of L is non empty set

[: the carrier of p, the carrier of L:] is non empty Relation-like set

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

pc is non empty Relation-like the carrier of p -defined the carrier of L -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of L) Element of bool [: the carrier of p, the carrier of L:]

bool the carrier of L is non empty set

pc .: Lc is Element of bool the carrier of L

cpc is Element of bool the carrier of L

X9 is Element of the carrier of L

pc " is Relation-like Function-like set

(pc ") . X9 is set

rng pc is non empty Element of bool the carrier of L

dom pc is non empty Element of bool the carrier of p

x9 is Element of the carrier of p

pc . x9 is Element of the carrier of L

y is Element of the carrier of p

pc . y is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of p

pc . y is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

x9 is set

pc . x9 is set

y9 is Element of the carrier of p

L is non empty transitive RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

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

p is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

Image p is non empty strict transitive full SubRelStr of L

rng p is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

subrelstr (rng p) is non empty strict transitive full SubRelStr of L

corestr p is non empty Relation-like the carrier of L -defined the carrier of (Image p) -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of (Image p)) V26( the carrier of (Image p)) Element of bool [: the carrier of L, the carrier of (Image p):]

the carrier of (Image p) is non empty set

[: the carrier of L, the carrier of (Image p):] is non empty Relation-like set

bool [: the carrier of L, the carrier of (Image p):] is non empty set

the carrier of (Image p) |` p is Relation-like the carrier of L -defined the carrier of L -valued the carrier of (Image p) -valued the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

Lc is Element of bool the carrier of L

(corestr p) .: Lc is Element of bool the carrier of (Image p)

bool the carrier of (Image p) is non empty set

"/\" (((corestr p) .: Lc),(Image p)) is Element of the carrier of (Image p)

"/\" (Lc,L) is Element of the carrier of L

(corestr p) . ("/\" (Lc,L)) is Element of the carrier of (Image p)

p .: Lc is Element of bool the carrier of L

dom p is non empty Element of bool the carrier of L

p . ("/\" (Lc,L)) is Element of the carrier of L

cpc is Element of bool the carrier of (Image p)

"/\" (cpc,L) is Element of the carrier of L

"/\" ((p .: Lc),L) is Element of the carrier of L

L is non empty transitive RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

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

p is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

Image p is non empty strict transitive full SubRelStr of L

rng p is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

subrelstr (rng p) is non empty strict transitive full SubRelStr of L

corestr p is non empty Relation-like the carrier of L -defined the carrier of (Image p) -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of (Image p)) V26( the carrier of (Image p)) Element of bool [: the carrier of L, the carrier of (Image p):]

the carrier of (Image p) is non empty set

[: the carrier of L, the carrier of (Image p):] is non empty Relation-like set

bool [: the carrier of L, the carrier of (Image p):] is non empty set

the carrier of (Image p) |` p is Relation-like the carrier of L -defined the carrier of L -valued the carrier of (Image p) -valued the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

Lc is Element of bool the carrier of L

(corestr p) .: Lc is Element of bool the carrier of (Image p)

bool the carrier of (Image p) is non empty set

"/\" (((corestr p) .: Lc),(Image p)) is Element of the carrier of (Image p)

"/\" (Lc,L) is Element of the carrier of L

(corestr p) . ("/\" (Lc,L)) is Element of the carrier of (Image p)

p .: Lc is Element of bool the carrier of L

dom p is non empty Element of bool the carrier of L

p . ("/\" (Lc,L)) is Element of the carrier of L

cpc is Element of bool the carrier of (Image p)

"/\" (cpc,L) is Element of the carrier of L

"/\" ((p .: Lc),L) is Element of the carrier of L

L is non empty transitive RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

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

p is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

Image p is non empty strict transitive full SubRelStr of L

rng p is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

subrelstr (rng p) is non empty strict transitive full SubRelStr of L

corestr p is non empty Relation-like the carrier of L -defined the carrier of (Image p) -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of (Image p)) V26( the carrier of (Image p)) Element of bool [: the carrier of L, the carrier of (Image p):]

the carrier of (Image p) is non empty set

[: the carrier of L, the carrier of (Image p):] is non empty Relation-like set

bool [: the carrier of L, the carrier of (Image p):] is non empty set

the carrier of (Image p) |` p is Relation-like the carrier of L -defined the carrier of L -valued the carrier of (Image p) -valued the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

Lc is Element of bool the carrier of L

(corestr p) .: Lc is Element of bool the carrier of (Image p)

bool the carrier of (Image p) is non empty set

"\/" (((corestr p) .: Lc),(Image p)) is Element of the carrier of (Image p)

"\/" (Lc,L) is Element of the carrier of L

(corestr p) . ("\/" (Lc,L)) is Element of the carrier of (Image p)

p .: Lc is Element of bool the carrier of L

dom p is non empty Element of bool the carrier of L

p . ("\/" (Lc,L)) is Element of the carrier of L

cpc is Element of bool the carrier of (Image p)

"\/" (cpc,L) is Element of the carrier of L

"\/" ((p .: Lc),L) is Element of the carrier of L

L is non empty transitive RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty Relation-like set

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

p is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

Image p is non empty strict transitive full SubRelStr of L

rng p is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

subrelstr (rng p) is non empty strict transitive full SubRelStr of L

corestr p is non empty Relation-like the carrier of L -defined the carrier of (Image p) -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of (Image p)) V26( the carrier of (Image p)) Element of bool [: the carrier of L, the carrier of (Image p):]

the carrier of (Image p) is non empty set

[: the carrier of L, the carrier of (Image p):] is non empty Relation-like set

bool [: the carrier of L, the carrier of (Image p):] is non empty set

the carrier of (Image p) |` p is Relation-like the carrier of L -defined the carrier of L -valued the carrier of (Image p) -valued the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

Lc is Element of bool the carrier of L

(corestr p) .: Lc is Element of bool the carrier of (Image p)

bool the carrier of (Image p) is non empty set

"\/" (((corestr p) .: Lc),(Image p)) is Element of the carrier of (Image p)

"\/" (Lc,L) is Element of the carrier of L

(corestr p) . ("\/" (Lc,L)) is Element of the carrier of (Image p)

p .: Lc is Element of bool the carrier of L

dom p is non empty Element of bool the carrier of L

p . ("\/" (Lc,L)) is Element of the carrier of L

cpc is Element of bool the carrier of (Image p)

"\/" (cpc,L) is Element of the carrier of L

"\/" ((p .: Lc),L) is Element of the carrier of L

L is non empty reflexive antisymmetric non void RelStr

the carrier of L is non empty set

p is non empty reflexive antisymmetric non void RelStr

the carrier of p is non empty set

[: the carrier of L, the carrier of p:] is non empty Relation-like set

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

Lc is non empty Relation-like the carrier of L -defined the carrier of p -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of p) Element of bool [: the carrier of L, the carrier of p:]

pc is Element of the carrier of L

cpc is Element of the carrier of L

Lc . pc is Element of the carrier of p

Lc . cpc is Element of the carrier of p

dom Lc is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

{pc,cpc} is non empty finite Element of bool the carrier of L

X9 is Element of the carrier of L

X9 is Element of the carrier of L

x is Element of the carrier of L

"/\" ({pc,cpc},L) is Element of the carrier of L

Lc .: {pc,cpc} is finite Element of bool the carrier of p

bool the carrier of p is non empty set

"/\" ((Lc .: {pc,cpc}),p) is Element of the carrier of p

{(Lc . pc),(Lc . cpc)} is non empty finite Element of bool the carrier of p

"/\" ({(Lc . pc),(Lc . cpc)},p) is Element of the carrier of p

L is non empty RelStr

the carrier of L is non empty set

p is non empty RelStr

the carrier of p is non empty set

[: the carrier of L, the carrier of p:] is non empty Relation-like set

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

bool the carrier of L is non empty set

Lc is non empty Relation-like the carrier of L -defined the carrier of p -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of p) Element of bool [: the carrier of L, the carrier of p:]

pc is Element of bool the carrier of L

Lc .: pc is Element of bool the carrier of p

bool the carrier of p is non empty set

cpc is Element of the carrier of p

X9 is Element of the carrier of p

x is set

Lc . x is set

x9 is set

Lc . x9 is set

y is Element of the carrier of L

x is Element of the carrier of L

y is Element of the carrier of L

Lc . y is Element of the carrier of p

x9 is Element of the carrier of p

L is non empty RelStr

the carrier of L is non empty set

p is non empty RelStr

the carrier of p is non empty set

[: the carrier of L, the carrier of p:] is non empty Relation-like set

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

Lc is non empty RelStr

the carrier of Lc is non empty set

[: the carrier of p, the carrier of Lc:] is non empty Relation-like set

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

pc is non empty Relation-like the carrier of L -defined the carrier of p -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of p) Element of bool [: the carrier of L, the carrier of p:]

cpc is non empty Relation-like the carrier of p -defined the carrier of Lc -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of Lc) Element of bool [: the carrier of p, the carrier of Lc:]

cpc * pc is non empty Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

[: the carrier of L, the carrier of Lc:] is non empty Relation-like set

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

bool the carrier of L is non empty set

x is Element of bool the carrier of L

(cpc * pc) .: x is Element of bool the carrier of Lc

bool the carrier of Lc is non empty set

"/\" (((cpc * pc) .: x),Lc) is Element of the carrier of Lc

"/\" (x,L) is Element of the carrier of L

(cpc * pc) . ("/\" (x,L)) is Element of the carrier of Lc

pc .: x is Element of bool the carrier of p

bool the carrier of p is non empty set

cpc .: (pc .: x) is Element of bool the carrier of Lc

dom pc is non empty Element of bool the carrier of L

"/\" ((pc .: x),p) is Element of the carrier of p

cpc . ("/\" ((pc .: x),p)) is Element of the carrier of Lc

pc . ("/\" (x,L)) is Element of the carrier of p

cpc . (pc . ("/\" (x,L))) is Element of the carrier of Lc

L is non empty reflexive antisymmetric non void RelStr

the carrier of L is non empty set

p is non empty reflexive antisymmetric non void RelStr

the carrier of p is non empty set

[: the carrier of L, the carrier of p:] is non empty Relation-like set

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

Lc is non empty reflexive antisymmetric non void RelStr

the carrier of Lc is non empty set

[: the carrier of p, the carrier of Lc:] is non empty Relation-like set

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

pc is non empty Relation-like the carrier of L -defined the carrier of p -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of p) Element of bool [: the carrier of L, the carrier of p:]

cpc is non empty Relation-like the carrier of p -defined the carrier of Lc -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of Lc) Element of bool [: the carrier of p, the carrier of Lc:]

cpc * pc is non empty Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

[: the carrier of L, the carrier of Lc:] is non empty Relation-like set

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

bool the carrier of L is non empty set

x is Element of bool the carrier of L

(cpc * pc) .: x is Element of bool the carrier of Lc

bool the carrier of Lc is non empty set

"/\" (((cpc * pc) .: x),Lc) is Element of the carrier of Lc

"/\" (x,L) is Element of the carrier of L

(cpc * pc) . ("/\" (x,L)) is Element of the carrier of Lc

the Element of x is Element of x

pc .: x is Element of bool the carrier of p

bool the carrier of p is non empty set

cpc .: (pc .: x) is Element of bool the carrier of Lc

pc . the Element of x is set

dom pc is non empty Element of bool the carrier of L

"/\" ((pc .: x),p) is Element of the carrier of p

cpc . ("/\" ((pc .: x),p)) is Element of the carrier of Lc

pc . ("/\" (x,L)) is Element of the carrier of p

cpc . (pc . ("/\" (x,L))) is Element of the carrier of Lc

L is non empty RelStr

the carrier of L is non empty set

p is non empty RelStr

the carrier of p is non empty set

[: the carrier of L, the carrier of p:] is non empty Relation-like set

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

Lc is non empty RelStr

the carrier of Lc is non empty set

[: the carrier of p, the carrier of Lc:] is non empty Relation-like set

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

pc is non empty Relation-like the carrier of L -defined the carrier of p -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of p) Element of bool [: the carrier of L, the carrier of p:]

cpc is non empty Relation-like the carrier of p -defined the carrier of Lc -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of Lc) Element of bool [: the carrier of p, the carrier of Lc:]

cpc * pc is non empty Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

[: the carrier of L, the carrier of Lc:] is non empty Relation-like set

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

bool the carrier of L is non empty set

x is Element of bool the carrier of L

(cpc * pc) .: x is Element of bool the carrier of Lc

bool the carrier of Lc is non empty set

"\/" (((cpc * pc) .: x),Lc) is Element of the carrier of Lc

"\/" (x,L) is Element of the carrier of L

(cpc * pc) . ("\/" (x,L)) is Element of the carrier of Lc

pc .: x is Element of bool the carrier of p

bool the carrier of p is non empty set

cpc .: (pc .: x) is Element of bool the carrier of Lc

dom pc is non empty Element of bool the carrier of L

"\/" ((pc .: x),p) is Element of the carrier of p

cpc . ("\/" ((pc .: x),p)) is Element of the carrier of Lc

pc . ("\/" (x,L)) is Element of the carrier of p

cpc . (pc . ("\/" (x,L))) is Element of the carrier of Lc

L is non empty reflexive antisymmetric non void RelStr

the carrier of L is non empty set

p is non empty reflexive antisymmetric non void RelStr

the carrier of p is non empty set

[: the carrier of L, the carrier of p:] is non empty Relation-like set

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

Lc is non empty reflexive antisymmetric non void RelStr

the carrier of Lc is non empty set

[: the carrier of p, the carrier of Lc:] is non empty Relation-like set

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

pc is non empty Relation-like the carrier of L -defined the carrier of p -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of p) Element of bool [: the carrier of L, the carrier of p:]

cpc is non empty Relation-like the carrier of p -defined the carrier of Lc -valued Function-like V17( the carrier of p) V25( the carrier of p, the carrier of Lc) Element of bool [: the carrier of p, the carrier of Lc:]

cpc * pc is non empty Relation-like the carrier of L -defined the carrier of Lc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of Lc) Element of bool [: the carrier of L, the carrier of Lc:]

[: the carrier of L, the carrier of Lc:] is non empty Relation-like set

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

bool the carrier of L is non empty set

x is Element of bool the carrier of L

(cpc * pc) .: x is Element of bool the carrier of Lc

bool the carrier of Lc is non empty set

"\/" (((cpc * pc) .: x),Lc) is Element of the carrier of Lc

"\/" (x,L) is Element of the carrier of L

(cpc * pc) . ("\/" (x,L)) is Element of the carrier of Lc

the Element of x is Element of x

pc .: x is Element of bool the carrier of p

bool the carrier of p is non empty set

cpc .: (pc .: x) is Element of bool the carrier of Lc

pc . the Element of x is set

dom pc is non empty Element of bool the carrier of L

"\/" ((pc .: x),p) is Element of the carrier of p

cpc . ("\/" ((pc .: x),p)) is Element of the carrier of Lc

pc . ("\/" (x,L)) is Element of the carrier of p

cpc . (pc . ("\/" (x,L))) is Element of the carrier of Lc

L is non empty set

p is Relation-like L -defined Function-like V17(L) RelStr-yielding non-Empty set

product p is non empty V141() strict RelStr

Lc is Relation-like L -defined Function-like V17(L) set

pc is Element of L

Lc . pc is set

p . pc is non empty RelStr

Bottom (p . pc) is Element of the carrier of (p . pc)

the carrier of (p . pc) is non empty set

"\/" ({},(p . pc)) is Element of the carrier of (p . pc)

dom Lc is Element of bool L

bool L is non empty set

the carrier of (product p) is non empty set

pc is Relation-like Function-like Element of the carrier of (product p)

cpc is Relation-like Function-like Element of the carrier of (product p)

X9 is Element of L

pc . X9 is Element of the carrier of (p . X9)

p . X9 is non empty RelStr

the carrier of (p . X9) is non empty set

Bottom (p . X9) is Element of the carrier of (p . X9)

"\/" ({},(p . X9)) is Element of the carrier of (p . X9)

cpc . X9 is Element of the carrier of (p . X9)

L is non empty set

p is Relation-like L -defined Function-like V17(L) RelStr-yielding non-Empty set

product p is non empty V141() strict RelStr

Lc is Relation-like L -defined Function-like V17(L) set

pc is Element of L

Lc . pc is set

p . pc is non empty RelStr

Top (p . pc) is Element of the carrier of (p . pc)

the carrier of (p . pc) is non empty set

"/\" ({},(p . pc)) is Element of the carrier of (p . pc)

dom Lc is Element of bool L

bool L is non empty set

the carrier of (product p) is non empty set

pc is Relation-like Function-like Element of the carrier of (product p)

cpc is Relation-like Function-like Element of the carrier of (product p)

X9 is Element of L

pc . X9 is Element of the carrier of (p . X9)

p . X9 is non empty RelStr

the carrier of (p . X9) is non empty set

Top (p . X9) is Element of the carrier of (p . X9)

"/\" ({},(p . X9)) is Element of the carrier of (p . X9)

cpc . X9 is Element of the carrier of (p . X9)

L is non empty set

p is Relation-like L -defined Function-like V17(L) RelStr-yielding non-Empty set

product p is non empty V141() strict RelStr

Bottom (product p) is Relation-like Function-like Element of the carrier of (product p)

the carrier of (product p) is non empty set

"\/" ({},(product p)) is Relation-like Function-like Element of the carrier of (product p)

Lc is Relation-like L -defined Function-like V17(L) set

pc is Element of L

Lc . pc is set

p . pc is non empty RelStr

Bottom (p . pc) is Element of the carrier of (p . pc)

the carrier of (p . pc) is non empty set

"\/" ({},(p . pc)) is Element of the carrier of (p . pc)

dom Lc is Element of bool L

bool L is non empty set

cpc is Element of L

(Bottom (product p)) . cpc is Element of the carrier of (p . cpc)

p . cpc is non empty RelStr

the carrier of (p . cpc) is non empty set

Bottom (p . cpc) is Element of the carrier of (p . cpc)

"\/" ({},(p . cpc)) is Element of the carrier of (p . cpc)

pc is Relation-like Function-like Element of the carrier of (product p)

X9 is Relation-like Function-like Element of the carrier of (product p)

x is Element of L

pc . x is Element of the carrier of (p . x)

p . x is non empty RelStr

the carrier of (p . x) is non empty set

Bottom (p . x) is Element of the carrier of (p . x)

"\/" ({},(p . x)) is Element of the carrier of (p . x)

X9 . x is Element of the carrier of (p . x)

x is Element of L

p . x is non empty RelStr

X9 is Relation-like Function-like Element of the carrier of (product p)

x is Element of L

pc . x is Element of the carrier of (p . x)

p . x is non empty RelStr

the carrier of (p . x) is non empty set

Bottom (p . x) is Element of the carrier of (p . x)

"\/" ({},(p . x)) is Element of the carrier of (p . x)

X9 . x is Element of the carrier of (p . x)

X9 is Relation-like Function-like Element of the carrier of (product p)

x is Element of L

pc . x is Element of the carrier of (p . x)

p . x is non empty RelStr

the carrier of (p . x) is non empty set

Bottom (p . x) is Element of the carrier of (p . x)

"\/" ({},(p . x)) is Element of the carrier of (p . x)

X9 . x is Element of the carrier of (p . x)

L is non empty set

p is Relation-like L -defined Function-like V17(L) RelStr-yielding non-Empty set

product p is non empty V141() strict RelStr

Top (product p) is Relation-like Function-like Element of the carrier of (product p)

the carrier of (product p) is non empty set

"/\" ({},(product p)) is Relation-like Function-like Element of the carrier of (product p)

Lc is Relation-like L -defined Function-like V17(L) set

pc is Element of L