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