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
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
cpc is Element of L
(Top (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
Top (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
Top (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
Top (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
Top (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 reflexive-yielding set
product p is non empty V141() strict reflexive non void RelStr
Lc is Element of L
p . Lc is non empty reflexive non void RelStr
the carrier of (product p) is non empty set
pc is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of pc is non empty set
cpc is Relation-like Function-like Element of the carrier of (product p)
X9 is Element of the carrier of pc
waybelow X9 is non empty directed lower Element of bool the carrier of pc
bool the carrier of pc is non empty set
{ b1 where b1 is Element of the carrier of pc : b1 is_way_below X9 } is set
waybelow cpc is Element of bool the carrier of (product p)
bool the carrier of (product p) is non empty set
{ b1 where b1 is Element of the carrier of (product p) : b1 is_way_below cpc } is set
cpc is Relation-like Function-like Element of the carrier of (product p)
waybelow cpc is Element of bool the carrier of (product p)
{ b1 where b1 is Element of the carrier of (product p) : b1 is_way_below cpc } is set
"\/" ((waybelow cpc),(product p)) is Relation-like Function-like Element of the carrier of (product p)
proj1 cpc is set
proj1 ("\/" ((waybelow cpc),(product p))) is set
x is set
bool L is non empty set
x9 is Element of L
{x9} is non empty finite Element of bool L
y is Relation-like L -defined Function-like V17(L) set
x is set
y +* (x,x) is Relation-like Function-like set
pi ((waybelow cpc),x9) is Element of bool the carrier of (p . x9)
p . x9 is non empty reflexive non void RelStr
the carrier of (p . x9) is non empty set
bool the carrier of (p . x9) is non empty set
y9 is Relation-like Function-like set
y9 . x is set
x1 is Relation-like Function-like Element of the carrier of (product p)
x1 . x9 is Element of the carrier of (p . x9)
cpc . x9 is Element of the carrier of (p . x9)
waybelow (cpc . x9) is Element of bool the carrier of (p . x9)
{ b1 where b1 is Element of the carrier of (p . x9) : b1 is_way_below cpc . x9 } is set
dom y is Element of bool L
proj1 (y +* (x,x)) is set
y9 is Element of L
(y +* (x,x)) . y9 is set
p . y9 is non empty reflexive non void RelStr
the carrier of (p . y9) is non empty set
y9 is Element of L
(y +* (x,x)) . y9 is set
y . y9 is set
p . y9 is non empty reflexive non void RelStr
Bottom (p . y9) is Element of the carrier of (p . y9)
the carrier of (p . y9) is non empty set
"\/" ({},(p . y9)) is Element of the carrier of (p . y9)
y9 is Element of L
x1 is Element of L
y9 is Relation-like Function-like Element of the carrier of (product p)
y9 . x9 is Element of the carrier of (p . x9)
p . x1 is non empty reflexive non void RelStr
y9 . x1 is Element of the carrier of (p . x1)
the carrier of (p . x1) is non empty set
cpc . x1 is Element of the carrier of (p . x1)
x1 is Element of L
p . x1 is non empty reflexive non void RelStr
y9 is Relation-like Function-like Element of the carrier of (product p)
y9 . x1 is Element of the carrier of (p . x1)
the carrier of (p . x1) is non empty set
y . x1 is set
Bottom (p . x1) is Element of the carrier of (p . x1)
"\/" ({},(p . x1)) is Element of the carrier of (p . x1)
cpc . x1 is Element of the carrier of (p . x1)
x1 is Element of L
y9 is Relation-like Function-like Element of the carrier of (product p)
y9 is Relation-like Function-like Element of the carrier of (product p)
x1 is Element of L
y is finite Element of bool L
y9 . x1 is Element of the carrier of (p . x1)
p . x1 is non empty reflexive non void RelStr
the carrier of (p . x1) is non empty set
y . x1 is set
Bottom (p . x1) is Element of the carrier of (p . x1)
"\/" ({},(p . x1)) is Element of the carrier of (p . x1)
y9 . x9 is Element of the carrier of (p . x9)
("\/" ((waybelow cpc),(product p))) . x9 is Element of the carrier of (p . x9)
"\/" ((pi ((waybelow cpc),x9)),(p . x9)) is Element of the carrier of (p . x9)
cpc . x is set
("\/" ((waybelow cpc),(product p))) . x is set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
p is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of p is non empty set
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
[:p,p:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:p,p:] is non empty set
id the carrier of p is non empty Relation-like the carrier of p -defined the carrier of p -valued V17( the carrier of p) V25( the carrier of p, the carrier of p) reflexive symmetric antisymmetric transitive Element of bool [: the carrier of p, the carrier of p:]
[: the carrier of p, the carrier of p:] is non empty Relation-like set
bool [: the carrier of p, 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) CLHomomorphism of L,p
(L,L,p,p,Lc,Lc) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:p,p:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:p,p:]) Element of bool [: the carrier of [:L,L:], the carrier of [:p,p:]:]
[: the carrier of [:L,L:], the carrier of [:p,p:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:p,p:]:] is non empty set
(L,L,p,p,Lc,Lc) " (id the carrier of p) is Element of bool the carrier of [:L,L:]
pc is Element of bool the carrier of [:L,L:]
subrelstr pc is strict reflexive transitive antisymmetric full SubRelStr of [:L,L:]
the Element of the carrier of L is Element of the carrier of L
dom Lc is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[ the Element of the carrier of L, the Element of the carrier of L] is V1() Element of the carrier of [:L,L:]
{ the Element of the carrier of L, the Element of the carrier of L} is non empty finite set
{ the Element of the carrier of L} is non empty finite set
{{ the Element of the carrier of L, the Element of the carrier of L},{ the Element of the carrier of L}} is non empty finite V34() set
[:(dom Lc),(dom Lc):] is non empty Relation-like Element of bool the carrier of [:L,L:]
Lc . the Element of the carrier of L is Element of the carrier of p
[(Lc . the Element of the carrier of L),(Lc . the Element of the carrier of L)] is V1() Element of the carrier of [:p,p:]
{(Lc . the Element of the carrier of L),(Lc . the Element of the carrier of L)} is non empty finite set
{(Lc . the Element of the carrier of L)} is non empty finite set
{{(Lc . the Element of the carrier of L),(Lc . the Element of the carrier of L)},{(Lc . the Element of the carrier of L)}} is non empty finite V34() set
dom (L,L,p,p,Lc,Lc) is non empty Element of bool the carrier of [:L,L:]
(L,L,p,p,Lc,Lc) . ( the Element of the carrier of L, the Element of the carrier of L) is set
[ the Element of the carrier of L, the Element of the carrier of L] is V1() set
(L,L,p,p,Lc,Lc) . [ the Element of the carrier of L, the Element of the carrier of L] is set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
X9 is non empty Element of bool the carrier of [:L,L:]
subrelstr X9 is non empty strict reflexive transitive antisymmetric full non void SubRelStr of [:L,L:]
the carrier of (subrelstr pc) is set
bool the carrier of (subrelstr pc) is non empty set
y is directed Element of bool the carrier of (subrelstr pc)
"\/" (y,[:L,L:]) is Element of the carrier of [:L,L:]
x is non empty directed Element of bool the carrier of [:L,L:]
(L,L,p,p,Lc,Lc) .: x is Element of bool the carrier of [:p,p:]
bool the carrier of [:p,p:] is non empty set
"\/" (((L,L,p,p,Lc,Lc) .: x),[:p,p:]) is Element of the carrier of [:p,p:]
"\/" (x,[:L,L:]) is Element of the carrier of [:L,L:]
(L,L,p,p,Lc,Lc) . ("\/" (x,[:L,L:])) is Element of the carrier of [:p,p:]
(L,L,p,p,Lc,Lc) .: y is Element of bool the carrier of [:p,p:]
(L,L,p,p,Lc,Lc) .: pc is Element of bool the carrier of [:p,p:]
y is set
x9 is set
[y,x9] is V1() set
{y,x9} is non empty finite set
{y} is non empty finite set
{{y,x9},{y}} is non empty finite V34() set
the carrier of (subrelstr pc) is set
bool the carrier of (subrelstr pc) is non empty set
y is Element of bool the carrier of (subrelstr pc)
"/\" (y,[:L,L:]) is Element of the carrier of [:L,L:]
(L,L,p,p,Lc,Lc) .: pc is Element of bool the carrier of [:p,p:]
bool the carrier of [:p,p:] is non empty set
x is Element of bool the carrier of [:L,L:]
(L,L,p,p,Lc,Lc) .: x is Element of bool the carrier of [:p,p:]
"/\" (((L,L,p,p,Lc,Lc) .: x),[:p,p:]) is Element of the carrier of [:p,p:]
"/\" (x,[:L,L:]) is Element of the carrier of [:L,L:]
(L,L,p,p,Lc,Lc) . ("/\" (x,[:L,L:])) is Element of the carrier of [:p,p:]
(L,L,p,p,Lc,Lc) .: y is Element of bool the carrier of [:p,p:]
y is set
x9 is set
[y,x9] is V1() set
{y,x9} is non empty finite set
{y} is non empty finite set
{{y,x9},{y}} is non empty finite V34() set
L is RelStr
[:L,L:] is strict RelStr
the carrier of [:L,L:] is set
bool the carrier of [:L,L:] is non empty set
p is Element of bool the carrier of [:L,L:]
the carrier of L is set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is non empty RelStr
[:L,L:] is non empty strict RelStr
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void 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
p is non empty Element of bool the carrier of [:L,L:]
(L,p) is 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 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
Lc is Element of the carrier of L
Class ((L,p),Lc) is Element of bool the carrier of L
bool the carrier of L is non empty set
"/\" ((Class ((L,p),Lc)),L) is Element of the carrier of L
[("/\" ((Class ((L,p),Lc)),L)),Lc] is V1() Element of the carrier of [:L,L:]
{("/\" ((Class ((L,p),Lc)),L)),Lc} is non empty finite set
{("/\" ((Class ((L,p),Lc)),L))} is non empty finite set
{{("/\" ((Class ((L,p),Lc)),L)),Lc},{("/\" ((Class ((L,p),Lc)),L))}} is non empty finite V34() set
{Lc} is non empty finite Element of bool the carrier of L
[:(Class ((L,p),Lc)),{Lc}:] is Relation-like Element of bool the carrier of [:L,L:]
cpc is Element of bool the carrier of [:L,L:]
subrelstr p is non empty strict reflexive transitive antisymmetric full non void SubRelStr of [:L,L:]
the carrier of (subrelstr p) is non empty set
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
bool the carrier of (subrelstr p) is non empty set
X9 is Element of bool the carrier of (subrelstr p)
"/\" (X9,[:L,L:]) is Element of the carrier of [:L,L:]
"/\" (cpc,[:L,L:]) is Element of the carrier of [:L,L:]
proj1 cpc is Element of bool the carrier of L
"/\" ((proj1 cpc),L) is Element of the carrier of L
proj2 cpc is Element of bool the carrier of L
"/\" ((proj2 cpc),L) is Element of the carrier of L
[("/\" ((proj1 cpc),L)),("/\" ((proj2 cpc),L))] is V1() Element of the carrier of [:L,L:]
{("/\" ((proj1 cpc),L)),("/\" ((proj2 cpc),L))} is non empty finite set
{("/\" ((proj1 cpc),L))} is non empty finite set
{{("/\" ((proj1 cpc),L)),("/\" ((proj2 cpc),L))},{("/\" ((proj1 cpc),L))}} is non empty finite V34() set
[("/\" ((Class ((L,p),Lc)),L)),("/\" ((proj2 cpc),L))] is V1() Element of the carrier of [:L,L:]
{("/\" ((Class ((L,p),Lc)),L)),("/\" ((proj2 cpc),L))} is non empty finite set
{{("/\" ((Class ((L,p),Lc)),L)),("/\" ((proj2 cpc),L))},{("/\" ((Class ((L,p),Lc)),L))}} is non empty finite V34() set
"/\" ({Lc},L) is Element of the carrier of L
[("/\" ((Class ((L,p),Lc)),L)),("/\" ({Lc},L))] is V1() Element of the carrier of [:L,L:]
{("/\" ((Class ((L,p),Lc)),L)),("/\" ({Lc},L))} is non empty finite set
{{("/\" ((Class ((L,p),Lc)),L)),("/\" ({Lc},L))},{("/\" ((Class ((L,p),Lc)),L))}} is non empty finite V34() set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
p is non empty Element of bool the carrier of [:L,L:]
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
(L,p) is 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 transitive Element of bool [: the carrier of L, the carrier of L:]
Lc 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:]
subrelstr p is non empty strict reflexive transitive antisymmetric full non void SubRelStr of [:L,L:]
pc 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:]
cpc is Element of the carrier of L
X9 is Element of the carrier of L
pc . cpc is Element of the carrier of L
pc . X9 is Element of the carrier of L
Class ((L,p),X9) is Element of bool the carrier of L
bool the carrier of L is non empty set
Class ((L,p),cpc) is Element of bool the carrier of L
"/\" ((Class ((L,p),cpc)),L) is Element of the carrier of L
[("/\" ((Class ((L,p),cpc)),L)),cpc] is V1() Element of the carrier of [:L,L:]
{("/\" ((Class ((L,p),cpc)),L)),cpc} is non empty finite set
{("/\" ((Class ((L,p),cpc)),L))} is non empty finite set
{{("/\" ((Class ((L,p),cpc)),L)),cpc},{("/\" ((Class ((L,p),cpc)),L))}} is non empty finite V34() set
"/\" ((Class ((L,p),X9)),L) is Element of the carrier of L
[("/\" ((Class ((L,p),X9)),L)),X9] is V1() Element of the carrier of [:L,L:]
{("/\" ((Class ((L,p),X9)),L)),X9} is non empty finite set
{("/\" ((Class ((L,p),X9)),L))} is non empty finite set
{{("/\" ((Class ((L,p),X9)),L)),X9},{("/\" ((Class ((L,p),X9)),L))}} is non empty finite V34() set
{[("/\" ((Class ((L,p),cpc)),L)),cpc],[("/\" ((Class ((L,p),X9)),L)),X9]} is non empty Relation-like finite Element of bool the carrier of [:L,L:]
y is Element of bool the carrier of [:L,L:]
"/\" (y,[:L,L:]) is Element of the carrier of [:L,L:]
proj1 y is Element of bool the carrier of L
"/\" ((proj1 y),L) is Element of the carrier of L
proj2 y is Element of bool the carrier of L
"/\" ((proj2 y),L) is Element of the carrier of L
[("/\" ((proj1 y),L)),("/\" ((proj2 y),L))] is V1() Element of the carrier of [:L,L:]
{("/\" ((proj1 y),L)),("/\" ((proj2 y),L))} is non empty finite set
{("/\" ((proj1 y),L))} is non empty finite set
{{("/\" ((proj1 y),L)),("/\" ((proj2 y),L))},{("/\" ((proj1 y),L))}} is non empty finite V34() set
{("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))} is non empty finite Element of bool the carrier of L
"/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L) is Element of the carrier of L
[("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),("/\" ((proj2 y),L))] is V1() Element of the carrier of [:L,L:]
{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),("/\" ((proj2 y),L))} is non empty finite set
{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L))} is non empty finite set
{{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),("/\" ((proj2 y),L))},{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L))}} is non empty finite V34() set
{cpc,X9} is non empty finite Element of bool the carrier of L
"/\" ({cpc,X9},L) is Element of the carrier of L
[("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),("/\" ({cpc,X9},L))] is V1() Element of the carrier of [:L,L:]
{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),("/\" ({cpc,X9},L))} is non empty finite set
{{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),("/\" ({cpc,X9},L))},{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L))}} is non empty finite V34() set
the carrier of (subrelstr p) is non empty set
bool the carrier of (subrelstr p) is non empty set
x is Element of bool the carrier of (subrelstr p)
"/\" (x,[:L,L:]) is Element of the carrier of [:L,L:]
cpc "/\" X9 is Element of the carrier of L
[("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),cpc] is V1() Element of the carrier of [:L,L:]
{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),cpc} is non empty finite set
{{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L)),cpc},{("/\" ({("/\" ((Class ((L,p),cpc)),L)),("/\" ((Class ((L,p),X9)),L))},L))}} is non empty finite V34() set
cpc is Element of the carrier of L
Class ((L,p),cpc) is Element of bool the carrier of L
bool the carrier of L is non empty set
"/\" ((Class ((L,p),cpc)),L) is Element of the carrier of L
[("/\" ((Class ((L,p),cpc)),L)),cpc] is V1() Element of the carrier of [:L,L:]
{("/\" ((Class ((L,p),cpc)),L)),cpc} is non empty finite set
{("/\" ((Class ((L,p),cpc)),L))} is non empty finite set
{{("/\" ((Class ((L,p),cpc)),L)),cpc},{("/\" ((Class ((L,p),cpc)),L))}} is non empty finite V34() set
Class ((L,p),("/\" ((Class ((L,p),cpc)),L))) is Element of bool the carrier of L
pc . cpc is Element of the carrier of L
pc . (pc . cpc) is Element of the carrier of L
"/\" ((Class ((L,p),("/\" ((Class ((L,p),cpc)),L)))),L) is Element of the carrier of L
pc * pc 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:]
(pc * pc) . cpc is Element of the carrier of L
cpc is Element of the carrier of L
Class ((L,p),cpc) is Element of bool the carrier of L
"/\" ((Class ((L,p),cpc)),L) is Element of the carrier of L
pc . cpc is Element of the carrier of L
id L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one V17( the carrier of L) V25( the carrier of L, the carrier of L) idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of L, the carrier of L:]
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:]
(id L) . cpc is Element of the carrier of L
cpc 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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
X9 is Element of the carrier of L
cpc . X9 is Element of the carrier of L
Class ((L,p),X9) is Element of bool the carrier of L
"/\" ((Class ((L,p),X9)),L) is Element of the carrier of L
Lc 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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
pc 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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
cpc is set
Lc . cpc is set
X9 is Element of the carrier of L
Class ((L,p),X9) is Element of bool the carrier of L
bool the carrier of L is non empty set
"/\" ((Class ((L,p),X9)),L) is Element of the carrier of L
pc . cpc is set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void 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 non empty Element of bool the carrier of [:L,L:]
(L,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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
(L,L,L,L,(L,p),(L,p)) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
[: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty set
(L,L,L,L,(L,p),(L,p)) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
dom (L,p) is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
(L,p) is 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 transitive Element of bool [: the carrier of L, the carrier of L:]
subrelstr p is non empty strict reflexive transitive antisymmetric full non void SubRelStr of [:L,L:]
cpc is Element of bool the carrier of L
(L,p) .: cpc is Element of bool the carrier of L
"\/" (((L,p) .: cpc),L) is Element of the carrier of L
"\/" (cpc,L) is Element of the carrier of L
(L,p) . ("\/" (cpc,L)) is Element of the carrier of L
X9 is set
{ [((L,p) . b1),b1] where b1 is Element of the carrier of L : b1 in cpc } is set
x9 is set
y is Element of the carrier of L
(L,p) . y is Element of the carrier of L
[((L,p) . y),y] is V1() Element of the carrier of [:L,L:]
{((L,p) . y),y} is non empty finite set
{((L,p) . y)} is non empty finite set
{{((L,p) . y),y},{((L,p) . y)}} is non empty finite V34() set
Class ((L,p),y) is Element of bool the carrier of L
"/\" ((Class ((L,p),y)),L) is Element of the carrier of L
the carrier of (subrelstr p) is non empty set
bool the carrier of (subrelstr p) is non empty set
y is Element of bool the carrier of [:L,L:]
x9 is Element of the carrier of L
(L,p) . x9 is Element of the carrier of L
[((L,p) . x9),x9] is V1() Element of the carrier of [:L,L:]
{((L,p) . x9),x9} is non empty finite set
{((L,p) . x9)} is non empty finite set
{{((L,p) . x9),x9},{((L,p) . x9)}} is non empty finite V34() set
x9 is Element of bool the carrier of (subrelstr p)
y9 is Element of the carrier of (subrelstr p)
x1 is Element of the carrier of (subrelstr p)
x2 is Element of the carrier of L
(L,p) . x2 is Element of the carrier of L
[((L,p) . x2),x2] is V1() Element of the carrier of [:L,L:]
{((L,p) . x2),x2} is non empty finite set
{((L,p) . x2)} is non empty finite set
{{((L,p) . x2),x2},{((L,p) . x2)}} is non empty finite V34() set
LR is Element of the carrier of L
(L,p) . LR is Element of the carrier of L
[((L,p) . LR),LR] is V1() Element of the carrier of [:L,L:]
{((L,p) . LR),LR} is non empty finite set
{((L,p) . LR)} is non empty finite set
{{((L,p) . LR),LR},{((L,p) . LR)}} is non empty finite V34() set
f9 is Element of the carrier of L
(L,p) . f9 is Element of the carrier of L
[((L,p) . f9),f9] is V1() Element of the carrier of [:L,L:]
{((L,p) . f9),f9} is non empty finite set
{((L,p) . f9)} is non empty finite set
{{((L,p) . f9),f9},{((L,p) . f9)}} is non empty finite V34() set
g is Element of the carrier of (subrelstr p)
y9 is set
proj1 y is Element of bool the carrier of L
x1 is set
[y9,x1] is V1() set
{y9,x1} is non empty finite set
{y9} is non empty finite set
{{y9,x1},{y9}} is non empty finite V34() set
x2 is Element of the carrier of L
(L,p) . x2 is Element of the carrier of L
[((L,p) . x2),x2] is V1() Element of the carrier of [:L,L:]
{((L,p) . x2),x2} is non empty finite set
{((L,p) . x2)} is non empty finite set
{{((L,p) . x2),x2},{((L,p) . x2)}} is non empty finite V34() set
x1 is set
(L,p) . x1 is set
x2 is Element of the carrier of L
(L,p) . x2 is Element of the carrier of L
[((L,p) . x2),x2] is V1() Element of the carrier of [:L,L:]
{((L,p) . x2),x2} is non empty finite set
{((L,p) . x2)} is non empty finite set
{{((L,p) . x2),x2},{((L,p) . x2)}} is non empty finite V34() set
y9 is set
proj2 y is Element of bool the carrier of L
x1 is set
[x1,y9] is V1() set
{x1,y9} is non empty finite set
{x1} is non empty finite set
{{x1,y9},{x1}} is non empty finite V34() set
x2 is Element of the carrier of L
(L,p) . x2 is Element of the carrier of L
[((L,p) . x2),x2] is V1() Element of the carrier of [:L,L:]
{((L,p) . x2),x2} is non empty finite set
{((L,p) . x2)} is non empty finite set
{{((L,p) . x2),x2},{((L,p) . x2)}} is non empty finite V34() set
x1 is Element of the carrier of L
(L,p) . x1 is Element of the carrier of L
[((L,p) . x1),x1] is V1() Element of the carrier of [:L,L:]
{((L,p) . x1),x1} is non empty finite set
{((L,p) . x1)} is non empty finite set
{{((L,p) . x1),x1},{((L,p) . x1)}} is non empty finite V34() set
"\/" (y,[:L,L:]) is Element of the carrier of [:L,L:]
[("\/" (((L,p) .: cpc),L)),("\/" (cpc,L))] is V1() Element of the carrier of [:L,L:]
{("\/" (((L,p) .: cpc),L)),("\/" (cpc,L))} is non empty finite set
{("\/" (((L,p) .: cpc),L))} is non empty finite set
{{("\/" (((L,p) .: cpc),L)),("\/" (cpc,L))},{("\/" (((L,p) .: cpc),L))}} is non empty finite V34() set
Class ((L,p),("\/" (cpc,L))) is Element of bool the carrier of L
y9 is Element of the carrier of L
x1 is set
(L,p) . x1 is set
x2 is Element of the carrier of L
"/\" ((Class ((L,p),("\/" (cpc,L)))),L) is Element of the carrier of L
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
x9 is Element of the carrier of L
(L,p) . x9 is Element of the carrier of L
Class ((L,p),x9) is Element of bool the carrier of L
"/\" ((Class ((L,p),x9)),L) is Element of the carrier of L
y is Element of the carrier of L
(L,p) . y is Element of the carrier of L
Class ((L,p),y) is Element of bool the carrier of L
"/\" ((Class ((L,p),y)),L) is Element of the carrier of L
[((L,p) . x9),((L,p) . y)] is V1() Element of the carrier of [:L,L:]
{((L,p) . x9),((L,p) . y)} is non empty finite set
{((L,p) . x9)} is non empty finite set
{{((L,p) . x9),((L,p) . y)},{((L,p) . x9)}} is non empty finite V34() set
dom (L,L,L,L,(L,p),(L,p)) is non empty Element of bool the carrier of [:L,L:]
[:(dom (L,p)),(dom (L,p)):] is non empty Relation-like Element of bool the carrier of [:L,L:]
[x9,y] is V1() Element of the carrier of [:L,L:]
{x9,y} is non empty finite set
{x9} is non empty finite set
{{x9,y},{x9}} is non empty finite V34() set
(L,L,L,L,(L,p),(L,p)) . (x9,y) is set
[x9,y] is V1() set
(L,L,L,L,(L,p),(L,p)) . [x9,y] is set
(L,L,L,L,(L,p),(L,p)) . 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
x9 is Element of the carrier of L
y is Element of the carrier of L
(L,L,L,L,(L,p),(L,p)) . (x9,y) is set
[x9,y] is V1() set
{x9,y} is non empty finite set
{x9} is non empty finite set
{{x9,y},{x9}} is non empty finite V34() set
(L,L,L,L,(L,p),(L,p)) . [x9,y] is set
(L,p) . x9 is Element of the carrier of L
(L,p) . y is Element of the carrier of L
[((L,p) . x9),((L,p) . y)] is V1() Element of the carrier of [:L,L:]
{((L,p) . x9),((L,p) . y)} is non empty finite set
{((L,p) . x9)} is non empty finite set
{{((L,p) . x9),((L,p) . y)},{((L,p) . x9)}} is non empty finite V34() set
Class ((L,p),x9) is Element of bool the carrier of L
"/\" ((Class ((L,p),x9)),L) is Element of the carrier of L
[((L,p) . x9),x9] is V1() Element of the carrier of [:L,L:]
{((L,p) . x9),x9} is non empty finite set
{{((L,p) . x9),x9},{((L,p) . x9)}} is non empty finite V34() set
[x9,((L,p) . x9)] is V1() Element of the carrier of [:L,L:]
{x9,((L,p) . x9)} is non empty finite set
{{x9,((L,p) . x9)},{x9}} is non empty finite V34() set
Class ((L,p),y) is Element of bool the carrier of L
"/\" ((Class ((L,p),y)),L) is Element of the carrier of L
[((L,p) . y),y] is V1() Element of the carrier of [:L,L:]
{((L,p) . y),y} is non empty finite set
{((L,p) . y)} is non empty finite set
{{((L,p) . y),y},{((L,p) . y)}} is non empty finite V34() set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void 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
[: 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
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:]
bool the carrier of L is non empty set
p is Element of bool the carrier of [:L,L:]
(L,p) is 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 transitive Element of bool [: the carrier of L, the carrier of L:]
Class (L,p) is a_partition of the carrier of L
Lc 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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
(L,L,L,L,Lc,Lc) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
[: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty set
(L,L,L,L,Lc,Lc) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
{ [(Class ((L,p),b1)),(Class ((L,p),b2))] where b1, b2 is Element of the carrier of L : Lc . b1 <= Lc . b2 } is set
rng Lc is non empty Element of bool the carrier of L
the Element of the carrier of L is Element of the carrier of L
Class ((L,p), the Element of the carrier of L) is Element of bool the carrier of L
bool (bool the carrier of L) is non empty set
x9 is non empty Element of bool (bool the carrier of L)
y is non empty strict RelStr
the carrier of y is non empty set
dom Lc is non empty Element of bool the carrier of L
cpc is non empty set
x is Element of x9
y is set
Class ((L,p),y) is Element of bool the carrier of L
x9 is Element of the carrier of L
Lc . x9 is Element of the carrier of L
y9 is Element of cpc
[:x9,cpc:] is non empty Relation-like set
bool [:x9,cpc:] is non empty set
x is non empty Relation-like x9 -defined cpc -valued Function-like V17(x9) V25(x9,cpc) Element of bool [:x9,cpc:]
dom (L,L,L,L,Lc,Lc) is non empty Element of bool the carrier of [:L,L:]
y is Element of the carrier of L
Class ((L,p),y) is Element of bool the carrier of L
x9 is Element of the carrier of L
Class ((L,p),x9) is Element of bool the carrier of L
Lc . y is Element of the carrier of L
Lc . x9 is Element of the carrier of L
[y,x9] is V1() Element of the carrier of [:L,L:]
{y,x9} is non empty finite set
{y} is non empty finite set
{{y,x9},{y}} is non empty finite V34() set
(L,L,L,L,Lc,Lc) . (y,x9) is set
[y,x9] is V1() set
(L,L,L,L,Lc,Lc) . [y,x9] is set
[(Lc . y),(Lc . x9)] is V1() Element of the carrier of [:L,L:]
{(Lc . y),(Lc . x9)} is non empty finite set
{(Lc . y)} is non empty finite set
{{(Lc . y),(Lc . x9)},{(Lc . y)}} is non empty finite V34() set
y is Element of the carrier of L
Class ((L,p),y) is Element of bool the carrier of L
x . (Class ((L,p),y)) is set
Lc . y is Element of the carrier of L
x9 is Element of x9
x . x9 is Element of cpc
y9 is Element of the carrier of L
Class ((L,p),y9) is Element of bool the carrier of L
Lc . y9 is Element of the carrier of L
y is Element of the carrier of y
x9 is set
Class ((L,p),x9) is Element of bool the carrier of L
y9 is Element of the carrier of L
Class ((L,p),y9) is Element of bool the carrier of L
y is set
x9 is set
x . y is set
x . x9 is set
y9 is Element of the carrier of y
x1 is Element of the carrier of L
Class ((L,p),x1) is Element of bool the carrier of L
x2 is Element of the carrier of y
LR is Element of the carrier of L
Class ((L,p),LR) is Element of bool the carrier of L
x . x2 is set
Lc . LR is Element of the carrier of L
x . y9 is set
Lc . x1 is Element of the carrier of L
the InternalRel of y is Relation-like the carrier of y -defined the carrier of y -valued Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty Relation-like set
bool [: the carrier of y, the carrier of y:] is non empty set
dom x is non empty Element of bool x9
bool x9 is non empty set
Image Lc is non empty strict reflexive transitive antisymmetric full non void SubRelStr of L
subrelstr (rng Lc) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of L
the carrier of (Image Lc) is non empty set
[: the carrier of y, the carrier of (Image Lc):] is non empty Relation-like set
bool [: the carrier of y, the carrier of (Image Lc):] is non empty set
y9 is set
x9 is non empty Relation-like the carrier of y -defined the carrier of (Image Lc) -valued Function-like V17( the carrier of y) V25( the carrier of y, the carrier of (Image Lc)) Element of bool [: the carrier of y, the carrier of (Image Lc):]
rng x9 is non empty Element of bool the carrier of (Image Lc)
bool the carrier of (Image Lc) is non empty set
dom x9 is non empty Element of bool the carrier of y
bool the carrier of y is non empty set
x1 is set
x9 . x1 is set
x2 is Element of the carrier of y
LR is Element of the carrier of L
Class ((L,p),LR) is Element of bool the carrier of L
x9 . x2 is Element of the carrier of (Image Lc)
Lc . LR is Element of the carrier of L
x1 is set
Lc . x1 is set
x2 is Element of the carrier of L
Class ((L,p),x2) is Element of bool the carrier of L
x9 . (Class ((L,p),x2)) is set
Lc . x2 is Element of the carrier of L
y9 is Element of the carrier of y
x1 is Element of the carrier of y
x9 . y9 is Element of the carrier of (Image Lc)
x9 . x1 is Element of the carrier of (Image Lc)
x2 is set
Class ((L,p),x2) is Element of bool the carrier of L
LR is Element of the carrier of L
Class ((L,p),LR) is Element of bool the carrier of L
f9 is Element of the carrier of L
Class ((L,p),f9) is Element of bool the carrier of L
Lc . LR is Element of the carrier of L
Lc . f9 is Element of the carrier of L
f9 is set
Class ((L,p),f9) is Element of bool the carrier of L
IR is Element of the carrier of L
Lc . IR is Element of the carrier of L
LR is Element of the carrier of L
Lc . LR is Element of the carrier of L
y9 is non empty strict reflexive transitive antisymmetric non void RelStr
x1 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
x2 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
LR is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of LR is non empty set
[: the carrier of (Image Lc), the carrier of LR:] is non empty Relation-like set
bool [: the carrier of (Image Lc), the carrier of LR:] is non empty set
x9 " is Relation-like Function-like set
f9 is non empty Relation-like the carrier of (Image Lc) -defined the carrier of LR -valued Function-like V17( the carrier of (Image Lc)) V25( the carrier of (Image Lc), the carrier of LR) Element of bool [: the carrier of (Image Lc), the carrier of LR:]
corestr Lc is non empty Relation-like the carrier of L -defined the carrier of (Image Lc) -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of (Image Lc)) V26( the carrier of (Image Lc)) monotone Element of bool [: the carrier of L, the carrier of (Image Lc):]
[: the carrier of L, the carrier of (Image Lc):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (Image Lc):] is non empty set
the carrier of (Image Lc) |` Lc is Relation-like the carrier of L -defined the carrier of L -valued the carrier of (Image Lc) -valued the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
the InternalRel of LR is non empty Relation-like the carrier of LR -defined the carrier of LR -valued Element of bool [: the carrier of LR, the carrier of LR:]
[: the carrier of LR, the carrier of LR:] is non empty Relation-like set
bool [: the carrier of LR, the carrier of LR:] is non empty set
[: the carrier of L, the carrier of LR:] is non empty Relation-like set
bool [: the carrier of L, the carrier of LR:] is non empty set
g is set
f9 is set
x9 is set
[f9,x9] is V1() set
{f9,x9} is non empty finite set
{f9} is non empty finite set
{{f9,x9},{f9}} is non empty finite V34() set
b is Element of the carrier of LR
a is Element of the carrier of LR
c24 is Element of the carrier of L
Class ((L,p),c24) is Element of bool the carrier of L
c25 is Element of the carrier of L
Class ((L,p),c25) is Element of bool the carrier of L
Lc . c24 is Element of the carrier of L
Lc . c25 is Element of the carrier of L
f9 is Element of the carrier of L
Class ((L,p),f9) is Element of bool the carrier of L
x9 is Element of the carrier of L
Class ((L,p),x9) is Element of bool the carrier of L
[(Class ((L,p),f9)),(Class ((L,p),x9))] is V1() Element of [:(bool the carrier of L),(bool the carrier of L):]
[:(bool the carrier of L),(bool the carrier of L):] is non empty Relation-like set
{(Class ((L,p),f9)),(Class ((L,p),x9))} is non empty finite set
{(Class ((L,p),f9))} is non empty finite set
{{(Class ((L,p),f9)),(Class ((L,p),x9))},{(Class ((L,p),f9))}} is non empty finite V34() set
Lc . f9 is Element of the carrier of L
Lc . x9 is Element of the carrier of L
a is Element of the carrier of LR
b is Element of the carrier of LR
g is non empty Relation-like the carrier of L -defined the carrier of LR -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of LR) Element of bool [: the carrier of L, the carrier of LR:]
f9 is set
x9 is Element of the carrier of L
Class ((L,p),x9) is Element of bool the carrier of L
x9 . (Class ((L,p),x9)) is set
Lc . x9 is Element of the carrier of L
dom (corestr Lc) is non empty Element of bool the carrier of L
f9 * (corestr Lc) is non empty Relation-like the carrier of L -defined the carrier of LR -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of LR) Element of bool [: the carrier of L, the carrier of LR:]
(f9 * (corestr Lc)) . f9 is set
(corestr Lc) . f9 is set
f9 . ((corestr Lc) . f9) is set
Lc . f9 is set
f9 . (Lc . f9) is set
g . f9 is set
f9 is non empty Relation-like the carrier of (Image Lc) -defined the carrier of LR -valued Function-like V17( the carrier of (Image Lc)) V25( the carrier of (Image Lc), the carrier of LR) sups-preserving join-preserving directed-sups-preserving Element of bool [: the carrier of (Image Lc), the carrier of LR:]
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void 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
[: 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:]
(L,p) is 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 transitive Element of bool [: the carrier of L, the carrier of L:]
Class (L,p) is a_partition of the carrier of L
subrelstr p is strict reflexive transitive antisymmetric full SubRelStr of [:L,L:]
pc is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of pc is non empty set
[: the carrier of L, the carrier of pc:] is non empty Relation-like set
bool [: the carrier of L, the carrier of pc:] is non empty set
bool the carrier of L is non empty set
x9 is set
Class ((L,p),x9) is Element of bool the carrier of L
[: the carrier of L,(Class (L,p)):] is Relation-like set
bool [: the carrier of L,(Class (L,p)):] is non empty set
x9 is Relation-like the carrier of L -defined Class (L,p) -valued Function-like V25( the carrier of L, Class (L,p)) Element of bool [: the carrier of L,(Class (L,p)):]
y is non empty Relation-like the carrier of L -defined the carrier of pc -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of pc) Element of bool [: the carrier of L, the carrier of pc:]
dom y is non empty Element of bool the carrier of L
y is set
x9 is set
y9 is set
[x9,y9] is V1() set
{x9,y9} is non empty finite set
{x9} is non empty finite set
{{x9,y9},{x9}} is non empty finite V34() set
x1 is Element of the carrier of L
y . x1 is Element of the carrier of pc
Class ((L,p),x1) is Element of bool the carrier of L
x2 is Element of the carrier of L
y . x2 is Element of the carrier of pc
Class ((L,p),x2) is Element of bool the carrier of L
[(y . x1),(y . x2)] is V1() Element of the carrier of [:pc,pc:]
[:pc,pc:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:pc,pc:] is non empty set
{(y . x1),(y . x2)} is non empty finite set
{(y . x1)} is non empty finite set
{{(y . x1),(y . x2)},{(y . x1)}} is non empty finite V34() set
id the carrier of pc is non empty Relation-like the carrier of pc -defined the carrier of pc -valued V17( the carrier of pc) V25( the carrier of pc, the carrier of pc) reflexive symmetric antisymmetric transitive Element of bool [: the carrier of pc, the carrier of pc:]
[: the carrier of pc, the carrier of pc:] is non empty Relation-like set
bool [: the carrier of pc, the carrier of pc:] is non empty set
(L,L,pc,pc,y,y) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:pc,pc:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:pc,pc:]) Element of bool [: the carrier of [:L,L:], the carrier of [:pc,pc:]:]
[: the carrier of [:L,L:], the carrier of [:pc,pc:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:pc,pc:]:] is non empty set
dom (L,L,pc,pc,y,y) is non empty Element of bool the carrier of [:L,L:]
[:(dom y),(dom y):] is non empty Relation-like Element of bool the carrier of [:L,L:]
[x1,x2] is V1() Element of the carrier of [:L,L:]
{x1,x2} is non empty finite set
{x1} is non empty finite set
{{x1,x2},{x1}} is non empty finite V34() set
(L,L,pc,pc,y,y) . (x1,x2) is set
[x1,x2] is V1() set
(L,L,pc,pc,y,y) . [x1,x2] is set
(L,L,pc,pc,y,y) " (id the carrier of pc) is Element of bool the carrier of [:L,L:]
(L,L,pc,pc,y,y) . y is set
x9 is set
y9 is set
[x9,y9] is V1() set
{x9,y9} is non empty finite set
{x9} is non empty finite set
{{x9,y9},{x9}} is non empty finite V34() set
x1 is Element of the carrier of L
y . x1 is Element of the carrier of pc
Class ((L,p),x1) is Element of bool the carrier of L
x2 is Element of the carrier of L
y . x2 is Element of the carrier of pc
Class ((L,p),x2) is Element of bool the carrier of L
(L,L,pc,pc,y,y) . (x1,x2) is set
[x1,x2] is V1() set
{x1,x2} is non empty finite set
{x1} is non empty finite set
{{x1,x2},{x1}} is non empty finite V34() set
(L,L,pc,pc,y,y) . [x1,x2] is set
[(y . x1),(y . x2)] is V1() Element of the carrier of [:pc,pc:]
{(y . x1),(y . x2)} is non empty finite set
{(y . x1)} is non empty finite set
{{(y . x1),(y . x2)},{(y . x1)}} is non empty finite V34() set
y is Element of the carrier of L
y . y is Element of the carrier of pc
Class ((L,p),y) is Element of bool the carrier of L
L is non empty reflexive non void 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
id L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one V17( the carrier of L) V25( the carrier of L, the carrier of L) idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of L, the carrier of L:]
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:]
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) idempotent monotone directed-sups-preserving projection kernel Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive non void 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
[:L,L:] is non empty strict reflexive non void RelStr
the carrier of [:L,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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
(L,L,L,L,p,p) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
[: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:L,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:]
(L,L,L,L,p,p) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
bool the carrier of [:L,L:] is non empty set
the Element of the carrier of L is Element of the carrier of L
dom p is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
p . the Element of the carrier of L is Element of the carrier of L
[(p . the Element of the carrier of L),(p . the Element of the carrier of L)] is V1() Element of the carrier of [:L,L:]
{(p . the Element of the carrier of L),(p . the Element of the carrier of L)} is non empty finite set
{(p . the Element of the carrier of L)} is non empty finite set
{{(p . the Element of the carrier of L),(p . the Element of the carrier of L)},{(p . the Element of the carrier of L)}} is non empty finite V34() set
(L,L,L,L,p,p) . ( the Element of the carrier of L, the Element of the carrier of L) is set
[ the Element of the carrier of L, the Element of the carrier of L] is V1() set
{ the Element of the carrier of L, the Element of the carrier of L} is non empty finite set
{ the Element of the carrier of L} is non empty finite set
{{ the Element of the carrier of L, the Element of the carrier of L},{ the Element of the carrier of L}} is non empty finite V34() set
(L,L,L,L,p,p) . [ the Element of the carrier of L, the Element of the carrier of L] is set
dom (L,L,L,L,p,p) is non empty Element of bool the carrier of [:L,L:]
[:(dom p),(dom p):] is non empty Relation-like Element of bool the carrier of [:L,L:]
[ the Element of the carrier of L, the Element of the carrier of L] is V1() Element of the carrier of [:L,L:]
L is non empty reflexive non void 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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
(L,p) is non empty Element of bool the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive non void RelStr
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
(L,L,L,L,p,p) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
[: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:L,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:]
(L,L,L,L,p,p) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous 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) idempotent monotone directed-sups-preserving projection kernel Element of bool [: the carrier of L, the carrier of L:]
(L,p) is non empty Element of bool the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
(L,L,L,L,p,p) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
[: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:L,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:]
(L,L,L,L,p,p) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
subrelstr (L,p) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of [:L,L:]
(L,(L,p)) is 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 transitive Element of bool [: the carrier of L, the carrier of L:]
Class (L,(L,p)) is a_partition of the carrier of L
bool the carrier of L is non empty set
{ [(Class ((L,(L,p)),b1)),(Class ((L,(L,p)),b2))] where b1, b2 is Element of the carrier of L : p . b1 <= p . b2 } is set
pc is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of pc is non empty set
the InternalRel of pc is non empty Relation-like the carrier of pc -defined the carrier of pc -valued Element of bool [: the carrier of pc, the carrier of pc:]
[: the carrier of pc, the carrier of pc:] is non empty Relation-like set
bool [: the carrier of pc, the carrier of pc:] is non empty set
[: the carrier of L, the carrier of pc:] is non empty Relation-like set
bool [: the carrier of L, the carrier of pc:] is non empty set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
p is non empty Element of bool the carrier of [:L,L:]
the carrier of L is non empty set
(L,p) is 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 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
Class (L,p) is a_partition of the carrier of L
(L,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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
(L,L,L,L,(L,p),(L,p)) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
[: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:L,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:]
(L,L,L,L,(L,p),(L,p)) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
bool the carrier of L is non empty set
{ [(Class ((L,p),b1)),(Class ((L,p),b2))] where b1, b2 is Element of the carrier of L : (L,p) . b1 <= (L,p) . b2 } is set
pc is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of pc is non empty set
the InternalRel of pc is non empty Relation-like the carrier of pc -defined the carrier of pc -valued Element of bool [: the carrier of pc, the carrier of pc:]
[: the carrier of pc, the carrier of pc:] is non empty Relation-like set
bool [: the carrier of pc, the carrier of pc:] is non empty set
[: the carrier of L, the carrier of pc:] is non empty Relation-like set
bool [: the carrier of L, the carrier of pc:] is non empty set
cpc is Element of the carrier of pc
X9 is Element of the carrier of pc
"/\" (cpc,L) is Element of the carrier of L
"/\" (X9,L) is Element of the carrier of L
x is set
Class ((L,p),x) is Element of bool the carrier of L
x9 is set
Class ((L,p),x9) is Element of bool the carrier of L
[cpc,X9] is V1() Element of the carrier of [:pc,pc:]
[:pc,pc:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:pc,pc:] is non empty set
{cpc,X9} is non empty finite set
{cpc} is non empty finite set
{{cpc,X9},{cpc}} is non empty finite V34() set
y is Element of the carrier of L
Class ((L,p),y) is Element of bool the carrier of L
x is Element of the carrier of L
Class ((L,p),x) is Element of bool the carrier of L
[(Class ((L,p),y)),(Class ((L,p),x))] is V1() Element of [:(bool the carrier of L),(bool the carrier of L):]
[:(bool the carrier of L),(bool the carrier of L):] is non empty Relation-like set
{(Class ((L,p),y)),(Class ((L,p),x))} is non empty finite set
{(Class ((L,p),y))} is non empty finite set
{{(Class ((L,p),y)),(Class ((L,p),x))},{(Class ((L,p),y))}} is non empty finite V34() set
(L,p) . y is Element of the carrier of L
(L,p) . x is Element of the carrier of L
"/\" ((Class ((L,p),y)),L) is Element of the carrier of L
y is Element of the carrier of L
(L,p) . y is Element of the carrier of L
Class ((L,p),y) is Element of bool the carrier of L
"/\" ((Class ((L,p),y)),L) is Element of the carrier of L
x is Element of the carrier of L
(L,p) . x is Element of the carrier of L
Class ((L,p),x) is Element of bool the carrier of L
"/\" ((Class ((L,p),x)),L) is Element of the carrier of L
Lc is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of Lc is non empty set
pc is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of pc is non empty set
x is set
the InternalRel of Lc is non empty Relation-like the carrier of Lc -defined the carrier of Lc -valued Element of bool [: the carrier of Lc, the carrier of Lc:]
[: the carrier of Lc, the carrier of Lc:] is non empty Relation-like set
bool [: the carrier of Lc, the carrier of Lc:] is non empty set
x9 is set
y is set
[x9,y] is V1() set
{x9,y} is non empty finite set
{x9} is non empty finite set
{{x9,y},{x9}} is non empty finite V34() set
x is Element of the carrier of Lc
y is Element of the carrier of Lc
"/\" (x,L) is Element of the carrier of L
"/\" (y,L) is Element of the carrier of L
x9 is Element of the carrier of pc
y9 is Element of the carrier of pc
the InternalRel of pc is non empty Relation-like the carrier of pc -defined the carrier of pc -valued Element of bool [: the carrier of pc, the carrier of pc:]
[: the carrier of pc, the carrier of pc:] is non empty Relation-like set
bool [: the carrier of pc, the carrier of pc:] is non empty set
x9 is set
y is set
[x9,y] is V1() set
{x9,y} is non empty finite set
{x9} is non empty finite set
{{x9,y},{x9}} is non empty finite V34() set
x is Element of the carrier of pc
y is Element of the carrier of pc
"/\" (x,L) is Element of the carrier of L
"/\" (y,L) is Element of the carrier of L
x9 is Element of the carrier of Lc
y9 is Element of the carrier of Lc
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void 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
p is non empty Element of bool the carrier of [:L,L:]
(L,p) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
the carrier of (L,p) is non empty set
(L,p) is 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 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
Class (L,p) is a_partition of the carrier of L
Lc is set
pc is set
Class ((L,p),pc) is Element of bool the carrier of L
bool the carrier of L is non empty set
cpc is Element of the carrier of L
X9 is Element of the carrier of L
Class ((L,p),X9) is Element of bool the carrier of L
pc is Element of the carrier of L
Class ((L,p),pc) is Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous RelStr
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
p is non empty Element of bool the carrier of [:L,L:]
(L,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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
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
(L,(L,p)) is non empty Element of bool the carrier of [:L,L:]
(L,L,L,L,(L,p),(L,p)) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
[: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:L,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:]
(L,L,L,L,(L,p),(L,p)) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous 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) idempotent monotone directed-sups-preserving projection kernel Element of bool [: the carrier of L, the carrier of L:]
(L,p) is non empty Element of bool the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void RelStr
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
(L,L,L,L,p,p) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
[: the carrier of [:L,L:], the carrier of [:L,L:]:] is non empty Relation-like set
bool [: the carrier of [:L,L:], the carrier of [:L,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:]
(L,L,L,L,p,p) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
(L,(L,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) idempotent monotone projection kernel Element of bool [: the carrier of L, the carrier of L:]
dom p is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
id L is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one V17( the carrier of L) V25( the carrier of L, the carrier of L) idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of L, the carrier of L:]
(L,L,L,L,(L,(L,p)),(L,(L,p))) is non empty Relation-like the carrier of [:L,L:] -defined the carrier of [:L,L:] -valued Function-like V17( the carrier of [:L,L:]) V25( the carrier of [:L,L:], the carrier of [:L,L:]) Element of bool [: the carrier of [:L,L:], the carrier of [:L,L:]:]
(L,L,L,L,(L,(L,p)),(L,(L,p))) " (id the carrier of L) is Element of bool the carrier of [:L,L:]
X9 is 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 transitive Element of bool [: the carrier of L, the carrier of L:]
field X9 is set
dom (L,L,L,L,(L,(L,p)),(L,(L,p))) is non empty Element of bool the carrier of [:L,L:]
dom (L,(L,p)) is non empty Element of bool the carrier of L
[:(dom (L,(L,p))),(dom (L,(L,p))):] is non empty Relation-like Element of bool the carrier of [:L,L:]
dom (L,L,L,L,p,p) is non empty Element of bool the carrier of [:L,L:]
[:(dom p),(dom p):] is non empty Relation-like Element of bool the carrier of [:L,L:]
x is set
x9 is Element of the carrier of L
p . x9 is Element of the carrier of L
p . (p . x9) is Element of the carrier of L
p * 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:]
(p * p) . x9 is Element of the carrier of L
[(p . x9),(p . x9)] is V1() Element of the carrier of [:L,L:]
{(p . x9),(p . x9)} is non empty finite set
{(p . x9)} is non empty finite set
{{(p . x9),(p . x9)},{(p . x9)}} is non empty finite V34() set
(L,L,L,L,p,p) . ((p . x9),x9) is set
[(p . x9),x9] is V1() set
{(p . x9),x9} is non empty finite set
{{(p . x9),x9},{(p . x9)}} is non empty finite V34() set
(L,L,L,L,p,p) . [(p . x9),x9] is set
[(p . (p . x9)),(p . x9)] is V1() Element of the carrier of [:L,L:]
{(p . (p . x9)),(p . x9)} is non empty finite set
{(p . (p . x9))} is non empty finite set
{{(p . (p . x9)),(p . x9)},{(p . (p . x9))}} is non empty finite V34() set
[(p . x9),x9] is V1() Element of the carrier of [:L,L:]
(L,(L,p)) . x9 is Element of the carrier of L
(L,(L,p)) . ((L,(L,p)) . x9) is Element of the carrier of L
(L,(L,p)) * (L,(L,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:]
((L,(L,p)) * (L,(L,p))) . x9 is Element of the carrier of L
(L,(L,p)) . (p . x9) is Element of the carrier of L
(id L) . (p . x9) is Element of the carrier of L
[((L,(L,p)) . x9),((L,(L,p)) . x9)] is V1() Element of the carrier of [:L,L:]
{((L,(L,p)) . x9),((L,(L,p)) . x9)} is non empty finite set
{((L,(L,p)) . x9)} is non empty finite set
{{((L,(L,p)) . x9),((L,(L,p)) . x9)},{((L,(L,p)) . x9)}} is non empty finite V34() set
(L,L,L,L,(L,(L,p)),(L,(L,p))) . (x9,((L,(L,p)) . x9)) is set
[x9,((L,(L,p)) . x9)] is V1() set
{x9,((L,(L,p)) . x9)} is non empty finite set
{x9} is non empty finite set
{{x9,((L,(L,p)) . x9)},{x9}} is non empty finite V34() set
(L,L,L,L,(L,(L,p)),(L,(L,p))) . [x9,((L,(L,p)) . x9)] is set
[((L,(L,p)) . x9),((L,(L,p)) . ((L,(L,p)) . x9))] is V1() Element of the carrier of [:L,L:]
{((L,(L,p)) . x9),((L,(L,p)) . ((L,(L,p)) . x9))} is non empty finite set
{{((L,(L,p)) . x9),((L,(L,p)) . ((L,(L,p)) . x9))},{((L,(L,p)) . x9)}} is non empty finite V34() set
[x9,((L,(L,p)) . x9)] is V1() Element of the carrier of [:L,L:]
[(p . x9),((L,(L,p)) . x9)] is V1() Element of the carrier of [:L,L:]
{(p . x9),((L,(L,p)) . x9)} is non empty finite set
{{(p . x9),((L,(L,p)) . x9)},{(p . x9)}} is non empty finite V34() set
(L,L,L,L,p,p) . ((p . x9),((L,(L,p)) . x9)) is set
[(p . x9),((L,(L,p)) . x9)] is V1() set
(L,L,L,L,p,p) . [(p . x9),((L,(L,p)) . x9)] is set
p . ((L,(L,p)) . x9) is Element of the carrier of L
[(p . (p . x9)),(p . ((L,(L,p)) . x9))] is V1() Element of the carrier of [:L,L:]
{(p . (p . x9)),(p . ((L,(L,p)) . x9))} is non empty finite set
{{(p . (p . x9)),(p . ((L,(L,p)) . x9))},{(p . (p . x9))}} is non empty finite V34() set
(L,L,L,L,(L,(L,p)),(L,(L,p))) . ((p . x9),((L,(L,p)) . x9)) is set
(L,L,L,L,(L,(L,p)),(L,(L,p))) . [(p . x9),((L,(L,p)) . x9)] is set
[((L,(L,p)) . (p . x9)),((L,(L,p)) . ((L,(L,p)) . x9))] is V1() Element of the carrier of [:L,L:]
{((L,(L,p)) . (p . x9)),((L,(L,p)) . ((L,(L,p)) . x9))} is non empty finite set
{((L,(L,p)) . (p . x9))} is non empty finite set
{{((L,(L,p)) . (p . x9)),((L,(L,p)) . ((L,(L,p)) . x9))},{((L,(L,p)) . (p . x9))}} is non empty finite V34() set
(id L) . ((L,(L,p)) . x9) is Element of the carrier of L
p . x is set
(L,(L,p)) . x is set
L is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V281() up-complete /\-complete non void satisfying_axiom_of_approximation continuous 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) idempotent monotone projection Element of bool [: the carrier of L, the carrier of L:]
Image p is non empty strict reflexive transitive antisymmetric full non void 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 reflexive transitive antisymmetric full non void SubRelStr of L
{ b1 where b1 is Element of the carrier of L : b1 <= p . b1 } is set
Lc is non empty Element of bool the carrier of L
subrelstr Lc is non empty strict reflexive transitive antisymmetric full non void SubRelStr of L
the carrier of (subrelstr Lc) is non empty set
[: the carrier of (subrelstr Lc), the carrier of (subrelstr Lc):] is non empty Relation-like set
bool [: the carrier of (subrelstr Lc), the carrier of (subrelstr Lc):] is non empty set
p | Lc is Relation-like the carrier of L -defined Lc -defined the carrier of L -defined the carrier of L -valued Function-like Element of bool [: the carrier of L, the carrier of L:]
pc is non empty Relation-like the carrier of (subrelstr Lc) -defined the carrier of (subrelstr Lc) -valued Function-like V17( the carrier of (subrelstr Lc)) V25( the carrier of (subrelstr Lc), the carrier of (subrelstr Lc)) Element of bool [: the carrier of (subrelstr Lc), the carrier of (subrelstr Lc):]
bool the carrier of (subrelstr Lc) is non empty set
cpc is Element of bool the carrier of (subrelstr Lc)
pc .: cpc is Element of bool the carrier of (subrelstr Lc)
"/\" ((pc .: cpc),(subrelstr Lc)) is Element of the carrier of (subrelstr Lc)
"/\" (cpc,(subrelstr Lc)) is Element of the carrier of (subrelstr Lc)
pc . ("/\" (cpc,(subrelstr Lc))) is Element of the carrier of (subrelstr Lc)
X9 is Element of bool the carrier of L
p .: cpc is Element of bool the carrier of L
"/\" (X9,L) is Element of the carrier of L
dom pc is non empty Element of bool the carrier of (subrelstr Lc)
"/\" ((pc .: cpc),L) is Element of the carrier of L
"/\" ((p .: cpc),L) is Element of the carrier of L
p . ("/\" (X9,L)) is Element of the carrier of L
Image pc is non empty strict reflexive transitive antisymmetric full non void SubRelStr of subrelstr Lc
rng pc is non empty Element of bool the carrier of (subrelstr Lc)
bool the carrier of (subrelstr Lc) is non empty set
subrelstr (rng pc) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of subrelstr Lc
the carrier of (Image pc) is non empty set
[: the carrier of (subrelstr Lc), the carrier of (Image pc):] is non empty Relation-like set
bool [: the carrier of (subrelstr Lc), the carrier of (Image pc):] is non empty set
corestr pc is non empty Relation-like the carrier of (subrelstr Lc) -defined the carrier of (Image pc) -valued Function-like V17( the carrier of (subrelstr Lc)) V25( the carrier of (subrelstr Lc), the carrier of (Image pc)) V26( the carrier of (Image pc)) Element of bool [: the carrier of (subrelstr Lc), the carrier of (Image pc):]
the carrier of (Image pc) |` pc is Relation-like the carrier of (subrelstr Lc) -defined the carrier of (subrelstr Lc) -valued the carrier of (Image pc) -valued the carrier of (subrelstr Lc) -valued Element of bool [: the carrier of (subrelstr Lc), the carrier of (subrelstr Lc):]
the carrier of (subrelstr (rng p)) is non empty set
the carrier of (subrelstr (rng pc)) is non empty set
cpc is non empty Relation-like the carrier of (subrelstr Lc) -defined the carrier of (Image pc) -valued Function-like V17( the carrier of (subrelstr Lc)) V25( the carrier of (subrelstr Lc), the carrier of (Image pc)) Element of bool [: the carrier of (subrelstr Lc), the carrier of (Image pc):]