K117() is set
bool K117() is non empty set
{} is set
the empty Function-like functional set is empty Function-like functional set
1 is non empty set
C is non quasi-empty ContextStr
f is strict non empty concept-like ConceptStr over C
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of (ConceptLattice C) is non empty set
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
Concept-with-all-Objects C is strict non empty concept-like V149(C) ConceptStr over C
(C,(Concept-with-all-Objects C)) is Element of the carrier of (ConceptLattice C)
the carrier of (ConceptLattice C) is non empty set
(C,(Concept-with-all-Objects C)) @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
f @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
(C,(Concept-with-all-Objects C)) "\/" f is Element of the carrier of (ConceptLattice C)
f "\/" (C,(Concept-with-all-Objects C)) is Element of the carrier of (ConceptLattice C)
Concept-with-all-Attributes C is strict non empty concept-like co-universal ConceptStr over C
(C,(Concept-with-all-Attributes C)) is Element of the carrier of (ConceptLattice C)
(C,(Concept-with-all-Attributes C)) @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
f @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
(C,(Concept-with-all-Attributes C)) "/\" f is Element of the carrier of (ConceptLattice C)
f "/\" (C,(Concept-with-all-Attributes C)) is Element of the carrier of (ConceptLattice C)
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
Bottom (ConceptLattice C) is Element of the carrier of (ConceptLattice C)
the carrier of (ConceptLattice C) is non empty set
Concept-with-all-Attributes C is strict non empty concept-like co-universal ConceptStr over C
Top (ConceptLattice C) is Element of the carrier of (ConceptLattice C)
Concept-with-all-Objects C is strict non empty concept-like V149(C) ConceptStr over C
(C,(Concept-with-all-Objects C)) is Element of the carrier of (ConceptLattice C)
(C,(Concept-with-all-Objects C)) @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
f @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
(C,(Concept-with-all-Objects C)) "\/" f is Element of the carrier of (ConceptLattice C)
f "\/" (C,(Concept-with-all-Objects C)) is Element of the carrier of (ConceptLattice C)
(C,(Concept-with-all-Attributes C)) is Element of the carrier of (ConceptLattice C)
(C,(Concept-with-all-Attributes C)) @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
f @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
(C,(Concept-with-all-Attributes C)) "/\" f is Element of the carrier of (ConceptLattice C)
f "/\" (C,(Concept-with-all-Attributes C)) is Element of the carrier of (ConceptLattice C)
C is non quasi-empty ContextStr
the carrier of C is non empty set
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
the carrier' of C is non empty set
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool the carrier' of C is non empty set
bool (bool the carrier' of C) is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
bool the carrier of C is non empty Element of bool (bool the carrier of C)
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
f is non empty Element of bool (bool the carrier of C)
union f is Element of bool the carrier of C
(ObjectDerivation C) . (union f) is Element of bool the carrier' of C
{ ((ObjectDerivation C) . b1) where b1 is Element of bool the carrier of C : b1 in f } is set
meet { ((ObjectDerivation C) . b1) where b1 is Element of bool the carrier of C : b1 in f } is set
b is set
a is non empty Element of bool (bool the carrier of C)
union a is Element of bool the carrier of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in union a or b2 is-connected-with b1 ) } is set
b is Element of the carrier' of C
a is Element of the carrier' of C
b is Element of bool the carrier of C
Av is Element of the carrier of C
v is Element of the carrier' of C
b is Element of bool the carrier of C
(ObjectDerivation C) . b is Element of bool the carrier' of C
Av is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in b or b2 is-connected-with b1 ) } is set
b is set
Av is Element of bool the carrier of C
(ObjectDerivation C) . Av is Element of bool the carrier' of C
the Element of { ((ObjectDerivation C) . b1) where b1 is Element of bool the carrier of C : b1 in f } is Element of { ((ObjectDerivation C) . b1) where b1 is Element of bool the carrier of C : b1 in f }
a is set
Av is Element of bool the carrier of C
(ObjectDerivation C) . Av is Element of bool the carrier' of C
b is Element of the carrier' of C
Av is Element of bool the carrier of C
(ObjectDerivation C) . Av is Element of bool the carrier' of C
Av is Element of bool the carrier of C
(ObjectDerivation C) . Av is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in Av or b2 is-connected-with b1 ) } is set
v is Element of the carrier of C
A is Element of the carrier' of C
Av is Element of the carrier of C
v is set
a is non empty Element of bool (bool the carrier of C)
union a is Element of bool the carrier of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in union a or b2 is-connected-with b1 ) } is set
the Element of f is Element of f
(ObjectDerivation C) . the Element of f is Element of bool the carrier' of C
C is non quasi-empty ContextStr
the carrier' of C is non empty set
bool the carrier' of C is non empty set
bool (bool the carrier' of C) is non empty set
the carrier of C is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
f is non empty Element of bool (bool the carrier' of C)
union f is Element of bool the carrier' of C
(AttributeDerivation C) . (union f) is Element of bool the carrier of C
{ ((AttributeDerivation C) . b1) where b1 is Element of bool the carrier' of C : b1 in f } is set
meet { ((AttributeDerivation C) . b1) where b1 is Element of bool the carrier' of C : b1 in f } is set
b is set
a is non empty Element of bool (bool the carrier' of C)
union a is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in union a or b1 is-connected-with b2 ) } is set
b is Element of the carrier of C
a is Element of the carrier of C
b is Element of bool the carrier' of C
Av is Element of the carrier' of C
v is Element of the carrier of C
b is Element of bool the carrier' of C
(AttributeDerivation C) . b is Element of bool the carrier of C
Av is Element of the carrier' of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in b or b1 is-connected-with b2 ) } is set
b is set
Av is Element of bool the carrier' of C
(AttributeDerivation C) . Av is Element of bool the carrier of C
the Element of { ((AttributeDerivation C) . b1) where b1 is Element of bool the carrier' of C : b1 in f } is Element of { ((AttributeDerivation C) . b1) where b1 is Element of bool the carrier' of C : b1 in f }
a is set
Av is Element of bool the carrier' of C
(AttributeDerivation C) . Av is Element of bool the carrier of C
b is Element of the carrier of C
Av is Element of bool the carrier' of C
(AttributeDerivation C) . Av is Element of bool the carrier of C
Av is Element of bool the carrier' of C
(AttributeDerivation C) . Av is Element of bool the carrier of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in Av or b1 is-connected-with b2 ) } is set
v is Element of the carrier' of C
A is Element of the carrier of C
Av is Element of the carrier' of C
v is set
a is non empty Element of bool (bool the carrier' of C)
union a is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in union a or b1 is-connected-with b2 ) } is set
the Element of f is Element of f
(AttributeDerivation C) . the Element of f is Element of bool the carrier of C
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
bool the carrier of (ConceptLattice C) is non empty set
f is Element of bool the carrier of (ConceptLattice C)
"/\" (f,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
{ b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than f } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than f } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
"\/" (f,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
bool the carrier of (ConceptLattice C) is non empty set
f is Element of bool the carrier of (ConceptLattice C)
"/\" (f,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
{ b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than f } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than f } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
"\/" (f,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
{} (ConceptLattice C) is empty proper Function-like functional initial final meet-closed join-closed Element of bool the carrier of (ConceptLattice C)
the carrier of (ConceptLattice C) is non empty set
bool the carrier of (ConceptLattice C) is non empty set
(C,({} (ConceptLattice C))) is non empty concept-like ConceptStr over C
"\/" (({} (ConceptLattice C)),(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
Concept-with-all-Attributes C is strict non empty concept-like co-universal ConceptStr over C
(C,({} (ConceptLattice C))) is non empty concept-like ConceptStr over C
"/\" (({} (ConceptLattice C)),(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
{ b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than {} (ConceptLattice C) } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than {} (ConceptLattice C) } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
Concept-with-all-Objects C is strict non empty concept-like V149(C) ConceptStr over C
(C,(Concept-with-all-Objects C)) is Element of the carrier of (ConceptLattice C)
f is Element of the carrier of (ConceptLattice C)
f @ is strict non empty concept-like ConceptStr over C
(C,(Concept-with-all-Objects C)) @ is strict non empty concept-like ConceptStr over C
f is Element of the carrier of (ConceptLattice C)
Bottom (ConceptLattice C) is Element of the carrier of (ConceptLattice C)
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
[#] the carrier of (ConceptLattice C) is non empty non proper Element of bool the carrier of (ConceptLattice C)
bool the carrier of (ConceptLattice C) is non empty set
(C,([#] the carrier of (ConceptLattice C))) is non empty concept-like ConceptStr over C
"\/" (([#] the carrier of (ConceptLattice C)),(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
Concept-with-all-Objects C is strict non empty concept-like V149(C) ConceptStr over C
(C,([#] the carrier of (ConceptLattice C))) is non empty concept-like ConceptStr over C
"/\" (([#] the carrier of (ConceptLattice C)),(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
{ b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than [#] the carrier of (ConceptLattice C) } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than [#] the carrier of (ConceptLattice C) } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
Concept-with-all-Attributes C is strict non empty concept-like co-universal ConceptStr over C
(C,(Concept-with-all-Attributes C)) is Element of the carrier of (ConceptLattice C)
f is Element of the carrier of (ConceptLattice C)
f @ is strict non empty concept-like ConceptStr over C
(C,(Concept-with-all-Attributes C)) @ is strict non empty concept-like ConceptStr over C
"\/" ( the carrier of (ConceptLattice C),(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
Top (ConceptLattice C) is Element of the carrier of (ConceptLattice C)
f is Element of the carrier of (ConceptLattice C)
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
bool the carrier of (ConceptLattice C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
the carrier' of C is non empty set
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool the carrier' of C is non empty set
bool (bool the carrier' of C) is non empty set
the carrier of C is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
f is non empty Element of bool the carrier of (ConceptLattice C)
(C,f) is non empty concept-like ConceptStr over C
"\/" (f,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
the Extent of (C,f) is Element of bool the carrier of C
{ the Extent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is set
union { the Extent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is set
(ObjectDerivation C) . (union { the Extent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } ) is set
(AttributeDerivation C) . ((ObjectDerivation C) . (union { the Extent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } )) is set
the Intent of (C,f) is Element of bool the carrier' of C
{ the Intent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is set
meet { the Intent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is set
the non empty concept-like Element of f is non empty concept-like Element of f
b is set
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
the Extent of ConceptStr(# a,b #) is Element of bool the carrier of C
b is set
Av is set
v is Element of bool the carrier of C
A is Element of bool the carrier' of C
ConceptStr(# v,A #) is strict ConceptStr over C
the Extent of ConceptStr(# v,A #) is Element of bool the carrier of C
Av is set
b is Element of bool the carrier of C
(ObjectDerivation C) . b is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . b) is Element of bool the carrier of C
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
b is set
the Extent of the non empty concept-like Element of f is Element of bool the carrier of C
b is Element of bool the carrier of C
Av is Element of bool the carrier' of C
ConceptStr(# b,Av #) is strict ConceptStr over C
b is Element of bool (bool the carrier of C)
{ ((ObjectDerivation C) . b1) where b1 is Element of bool the carrier of C : b1 in { the Extent of ConceptStr(# b1,b2 #) where b2 is Element of bool the carrier of C, b3 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } } is set
Av is set
v is Element of bool the carrier of C
A is Element of bool the carrier' of C
ConceptStr(# v,A #) is strict ConceptStr over C
the Intent of ConceptStr(# v,A #) is Element of bool the carrier' of C
the Extent of ConceptStr(# v,A #) is Element of bool the carrier of C
(ObjectDerivation C) . the Extent of ConceptStr(# v,A #) is Element of bool the carrier' of C
Av is set
v is Element of bool the carrier of C
(ObjectDerivation C) . v is Element of bool the carrier' of C
A is Element of bool the carrier of C
fb is Element of bool the carrier' of C
ConceptStr(# A,fb #) is strict ConceptStr over C
the Extent of ConceptStr(# A,fb #) is Element of bool the carrier of C
the Intent of ConceptStr(# A,fb #) is Element of bool the carrier' of C
b is non empty Element of bool (bool the carrier of C)
{ ((ObjectDerivation C) . b1) where b1 is Element of bool the carrier of C : b1 in b } is set
meet { ((ObjectDerivation C) . b1) where b1 is Element of bool the carrier of C : b1 in b } is set
the Element of { the Intent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is Element of { the Intent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f }
A is set
the Intent of the non empty concept-like Element of f is Element of bool the carrier' of C
fb is Element of bool the carrier of C
O9 is Element of bool the carrier' of C
ConceptStr(# fb,O9 #) is strict ConceptStr over C
fb is Element of bool the carrier of C
O9 is Element of bool the carrier' of C
ConceptStr(# fb,O9 #) is strict ConceptStr over C
the Intent of ConceptStr(# fb,O9 #) is Element of bool the carrier' of C
v is set
A is set
fb is Element of bool the carrier of C
O9 is Element of bool the carrier' of C
ConceptStr(# fb,O9 #) is strict ConceptStr over C
the Extent of ConceptStr(# fb,O9 #) is Element of bool the carrier of C
a is Element of bool the carrier of C
Av is Element of bool the carrier' of C
ConceptStr(# a,Av #) is strict ConceptStr over C
v is strict non empty concept-like ConceptStr over C
A is Element of the carrier of (ConceptLattice C)
A @ is strict non empty concept-like ConceptStr over C
the Intent of (A @) is Element of bool the carrier' of C
fb is Element of the carrier of (ConceptLattice C)
fb @ is strict non empty concept-like ConceptStr over C
the Intent of (fb @) is Element of bool the carrier' of C
O9 is Element of the carrier of (ConceptLattice C)
O9 @ is strict non empty concept-like ConceptStr over C
the Intent of (O9 @) is Element of bool the carrier' of C
A9 is set
fb is set
fa is Element of bool the carrier of C
fa is Element of bool the carrier' of C
ConceptStr(# fa,fa #) is strict ConceptStr over C
the Intent of ConceptStr(# fa,fa #) is Element of bool the carrier' of C
fb is Element of the carrier of (ConceptLattice C)
fb @ is strict non empty concept-like ConceptStr over C
the Intent of (fb @) is Element of bool the carrier' of C
the Intent of the non empty concept-like Element of f is Element of bool the carrier' of C
fb is Element of bool the carrier of C
fa is Element of bool the carrier' of C
ConceptStr(# fb,fa #) is strict ConceptStr over C
fb is Element of the carrier of (ConceptLattice C)
fb @ is strict non empty concept-like ConceptStr over C
the Intent of (fb @) is Element of bool the carrier' of C
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
bool the carrier of (ConceptLattice C) is non empty set
the carrier of C is non empty set
bool the carrier of C is non empty set
the carrier' of C is non empty set
bool the carrier' of C is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
f is non empty Element of bool the carrier of (ConceptLattice C)
(C,f) is non empty concept-like ConceptStr over C
"/\" (f,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
{ b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than f } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than f } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
the Extent of (C,f) is Element of bool the carrier of C
{ the Extent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is set
meet { the Extent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is set
the Intent of (C,f) is Element of bool the carrier' of C
{ the Intent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is set
union { the Intent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is set
(AttributeDerivation C) . (union { the Intent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } ) is set
(ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } )) is set
the non empty concept-like Element of f is non empty concept-like Element of f
b is set
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
the Intent of ConceptStr(# a,b #) is Element of bool the carrier' of C
b is set
Av is set
v is Element of bool the carrier of C
A is Element of bool the carrier' of C
ConceptStr(# v,A #) is strict ConceptStr over C
the Intent of ConceptStr(# v,A #) is Element of bool the carrier' of C
Av is set
b is Element of bool the carrier' of C
(AttributeDerivation C) . b is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . b) is Element of bool the carrier' of C
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
b is set
the Intent of the non empty concept-like Element of f is Element of bool the carrier' of C
b is Element of bool the carrier of C
Av is Element of bool the carrier' of C
ConceptStr(# b,Av #) is strict ConceptStr over C
b is Element of bool (bool the carrier' of C)
{ ((AttributeDerivation C) . b1) where b1 is Element of bool the carrier' of C : b1 in { the Intent of ConceptStr(# b1,b2 #) where b2 is Element of bool the carrier of C, b3 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } } is set
Av is set
v is Element of bool the carrier of C
A is Element of bool the carrier' of C
ConceptStr(# v,A #) is strict ConceptStr over C
the Extent of ConceptStr(# v,A #) is Element of bool the carrier of C
the Intent of ConceptStr(# v,A #) is Element of bool the carrier' of C
(AttributeDerivation C) . the Intent of ConceptStr(# v,A #) is Element of bool the carrier of C
Av is set
v is Element of bool the carrier' of C
(AttributeDerivation C) . v is Element of bool the carrier of C
A is Element of bool the carrier of C
fb is Element of bool the carrier' of C
ConceptStr(# A,fb #) is strict ConceptStr over C
the Intent of ConceptStr(# A,fb #) is Element of bool the carrier' of C
the Extent of ConceptStr(# A,fb #) is Element of bool the carrier of C
b is non empty Element of bool (bool the carrier' of C)
{ ((AttributeDerivation C) . b1) where b1 is Element of bool the carrier' of C : b1 in b } is set
meet { ((AttributeDerivation C) . b1) where b1 is Element of bool the carrier' of C : b1 in b } is set
the Element of { the Extent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f } is Element of { the Extent of ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) in f }
A is set
the Extent of the non empty concept-like Element of f is Element of bool the carrier of C
fb is Element of bool the carrier of C
O9 is Element of bool the carrier' of C
ConceptStr(# fb,O9 #) is strict ConceptStr over C
fb is Element of bool the carrier of C
O9 is Element of bool the carrier' of C
ConceptStr(# fb,O9 #) is strict ConceptStr over C
the Extent of ConceptStr(# fb,O9 #) is Element of bool the carrier of C
v is set
A is set
fb is Element of bool the carrier of C
O9 is Element of bool the carrier' of C
ConceptStr(# fb,O9 #) is strict ConceptStr over C
the Intent of ConceptStr(# fb,O9 #) is Element of bool the carrier' of C
Av is Element of bool the carrier of C
a is Element of bool the carrier' of C
ConceptStr(# Av,a #) is strict ConceptStr over C
v is strict non empty concept-like ConceptStr over C
A is Element of the carrier of (ConceptLattice C)
A @ is strict non empty concept-like ConceptStr over C
the Extent of (A @) is Element of bool the carrier of C
fb is Element of the carrier of (ConceptLattice C)
fb @ is strict non empty concept-like ConceptStr over C
the Extent of (fb @) is Element of bool the carrier of C
O9 is Element of the carrier of (ConceptLattice C)
O9 @ is strict non empty concept-like ConceptStr over C
the Extent of (O9 @) is Element of bool the carrier of C
A9 is set
fb is set
fa is Element of bool the carrier of C
fa is Element of bool the carrier' of C
ConceptStr(# fa,fa #) is strict ConceptStr over C
the Extent of ConceptStr(# fa,fa #) is Element of bool the carrier of C
fb is Element of the carrier of (ConceptLattice C)
fb @ is strict non empty concept-like ConceptStr over C
the Extent of (fb @) is Element of bool the carrier of C
the Extent of the non empty concept-like Element of f is Element of bool the carrier of C
fb is Element of bool the carrier of C
fa is Element of bool the carrier' of C
ConceptStr(# fb,fa #) is strict ConceptStr over C
fb is Element of the carrier of (ConceptLattice C)
fb @ is strict non empty concept-like ConceptStr over C
the Extent of (fb @) is Element of bool the carrier of C
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of C is non empty set
bool the carrier of C is non empty set
the carrier' of C is non empty set
bool the carrier' of C is non empty set
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
f is strict non empty concept-like ConceptStr over C
the Extent of f is Element of bool the carrier of C
{ ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ex b3 being Element of the carrier of C st
( b3 in the Extent of f & b1 = (AttributeDerivation C) . ((ObjectDerivation C) . {b3}) & b2 = (ObjectDerivation C) . {b3} ) } is set
"\/" ( { ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ex b3 being Element of the carrier of C st
( b3 in the Extent of f & b1 = (AttributeDerivation C) . ((ObjectDerivation C) . {b3}) & b2 = (ObjectDerivation C) . {b3} ) } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
the carrier of (ConceptLattice C) is non empty set
(C,f) is Element of the carrier of (ConceptLattice C)
b is Element of the carrier of (ConceptLattice C)
b @ is strict non empty concept-like ConceptStr over C
the Extent of (b @) is Element of bool the carrier of C
a is set
b is Element of the carrier of C
{b} is Element of bool the carrier of C
(ObjectDerivation C) . {b} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {b}) is Element of bool the carrier of C
ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . {b})),((ObjectDerivation C) . {b}) #) is strict ConceptStr over C
Av is strict non empty concept-like ConceptStr over C
(C,Av) is Element of the carrier of (ConceptLattice C)
(C,Av) @ is strict non empty concept-like ConceptStr over C
the Extent of Av is Element of bool the carrier of C
(C,f) @ is strict non empty concept-like ConceptStr over C
b is Element of the carrier of (ConceptLattice C)
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
a is Element of the carrier of C
{a} is Element of bool the carrier of C
(ObjectDerivation C) . {a} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {a}) is Element of bool the carrier of C
a is Element of the carrier of C
{a} is Element of bool the carrier of C
(ObjectDerivation C) . {a} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {a}) is Element of bool the carrier of C
(ObjectDerivation C) . the Extent of f is Element of bool the carrier' of C
the Intent of f is Element of bool the carrier' of C
b @ is strict non empty concept-like ConceptStr over C
the Intent of (b @) is Element of bool the carrier' of C
(C,f) @ is strict non empty concept-like ConceptStr over C
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of C is non empty set
bool the carrier of C is non empty set
the carrier' of C is non empty set
bool the carrier' of C is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
f is strict non empty concept-like ConceptStr over C
the Intent of f is Element of bool the carrier' of C
{ ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ex b3 being Element of the carrier' of C st
( b3 in the Intent of f & b1 = (AttributeDerivation C) . {b3} & b2 = (ObjectDerivation C) . ((AttributeDerivation C) . {b3}) ) } is set
"/\" ( { ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ex b3 being Element of the carrier' of C st
( b3 in the Intent of f & b1 = (AttributeDerivation C) . {b3} & b2 = (ObjectDerivation C) . ((AttributeDerivation C) . {b3}) ) } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
the carrier of (ConceptLattice C) is non empty set
{ b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than { ConceptStr(# b1,b2 #) where b2 is Element of bool the carrier of C, b3 is Element of bool the carrier' of C : ex b4 being Element of the carrier' of C st
( b3 in the Intent of f & b1 = (AttributeDerivation C) . {b3} & b2 = (ObjectDerivation C) . ((AttributeDerivation C) . {b3}) ) } } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than { ConceptStr(# b1,b2 #) where b2 is Element of bool the carrier of C, b3 is Element of bool the carrier' of C : ex b4 being Element of the carrier' of C st
( b3 in the Intent of f & b1 = (AttributeDerivation C) . {b3} & b2 = (ObjectDerivation C) . ((AttributeDerivation C) . {b3}) ) } } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
(C,f) is Element of the carrier of (ConceptLattice C)
b is Element of the carrier of (ConceptLattice C)
b @ is strict non empty concept-like ConceptStr over C
the Intent of (b @) is Element of bool the carrier' of C
a is set
b is Element of the carrier' of C
{b} is Element of bool the carrier' of C
(AttributeDerivation C) . {b} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {b}) is Element of bool the carrier' of C
ConceptStr(# ((AttributeDerivation C) . {b}),((ObjectDerivation C) . ((AttributeDerivation C) . {b})) #) is strict ConceptStr over C
Av is strict non empty concept-like ConceptStr over C
(C,Av) is Element of the carrier of (ConceptLattice C)
(C,Av) @ is strict non empty concept-like ConceptStr over C
the Intent of Av is Element of bool the carrier' of C
(C,f) @ is strict non empty concept-like ConceptStr over C
b is Element of the carrier of (ConceptLattice C)
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
a is Element of the carrier' of C
{a} is Element of bool the carrier' of C
(AttributeDerivation C) . {a} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {a}) is Element of bool the carrier' of C
a is Element of the carrier' of C
{a} is Element of bool the carrier' of C
(AttributeDerivation C) . {a} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {a}) is Element of bool the carrier' of C
(AttributeDerivation C) . the Intent of f is Element of bool the carrier of C
the Extent of f is Element of bool the carrier of C
b @ is strict non empty concept-like ConceptStr over C
the Extent of (b @) is Element of bool the carrier of C
(C,f) @ is strict non empty concept-like ConceptStr over C
C is non quasi-empty ContextStr
the carrier of C is non empty set
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
[: the carrier of C, the carrier of (ConceptLattice C):] is non empty set
bool [: the carrier of C, the carrier of (ConceptLattice C):] is non empty set
bool the carrier of C is non empty set
the carrier' of C is non empty set
bool the carrier' of C is non empty set
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
f is set
{f} is set
(ObjectDerivation C) . {f} is set
(AttributeDerivation C) . ((ObjectDerivation C) . {f}) is set
a is Element of bool the carrier of C
(ObjectDerivation C) . a is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . a) is Element of bool the carrier of C
ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . a)),((ObjectDerivation C) . a) #) is strict ConceptStr over C
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
f is non empty V7() V10( the carrier of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of (ConceptLattice C):]
a is Element of the carrier of C
f . a is Element of the carrier of (ConceptLattice C)
{a} is Element of bool the carrier of C
(ObjectDerivation C) . {a} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {a}) is Element of bool the carrier of C
f is non empty V7() V10( the carrier of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of (ConceptLattice C):]
a is non empty V7() V10( the carrier of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of (ConceptLattice C):]
b is set
f . b is set
a . b is set
a is Element of the carrier of C
f . a is Element of the carrier of (ConceptLattice C)
{a} is Element of bool the carrier of C
(ObjectDerivation C) . {a} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {a}) is Element of bool the carrier of C
a . a is Element of the carrier of (ConceptLattice C)
b is Element of bool the carrier of C
a is Element of bool the carrier' of C
ConceptStr(# b,a #) is strict ConceptStr over C
b is Element of bool the carrier of C
Av is Element of bool the carrier' of C
ConceptStr(# b,Av #) is strict ConceptStr over C
dom f is Element of bool the carrier of C
dom a is Element of bool the carrier of C
C is non quasi-empty ContextStr
the carrier' of C is non empty set
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
[: the carrier' of C, the carrier of (ConceptLattice C):] is non empty set
bool [: the carrier' of C, the carrier of (ConceptLattice C):] is non empty set
the carrier of C is non empty set
bool the carrier of C is non empty set
bool the carrier' of C is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
f is set
{f} is set
(AttributeDerivation C) . {f} is set
(ObjectDerivation C) . ((AttributeDerivation C) . {f}) is set
a is Element of bool the carrier' of C
(AttributeDerivation C) . a is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . a) is Element of bool the carrier' of C
ConceptStr(# ((AttributeDerivation C) . a),((ObjectDerivation C) . ((AttributeDerivation C) . a)) #) is strict ConceptStr over C
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
f is non empty V7() V10( the carrier' of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier' of C) quasi_total Element of bool [: the carrier' of C, the carrier of (ConceptLattice C):]
a is Element of the carrier' of C
f . a is Element of the carrier of (ConceptLattice C)
{a} is Element of bool the carrier' of C
(AttributeDerivation C) . {a} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {a}) is Element of bool the carrier' of C
f is non empty V7() V10( the carrier' of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier' of C) quasi_total Element of bool [: the carrier' of C, the carrier of (ConceptLattice C):]
a is non empty V7() V10( the carrier' of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier' of C) quasi_total Element of bool [: the carrier' of C, the carrier of (ConceptLattice C):]
b is set
f . b is set
a . b is set
a is Element of the carrier' of C
f . a is Element of the carrier of (ConceptLattice C)
{a} is Element of bool the carrier' of C
(AttributeDerivation C) . {a} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {a}) is Element of bool the carrier' of C
a . a is Element of the carrier of (ConceptLattice C)
b is Element of bool the carrier of C
a is Element of bool the carrier' of C
ConceptStr(# b,a #) is strict ConceptStr over C
b is Element of bool the carrier of C
Av is Element of bool the carrier' of C
ConceptStr(# b,Av #) is strict ConceptStr over C
dom f is Element of bool the carrier' of C
dom a is Element of bool the carrier' of C
C is non quasi-empty ContextStr
the carrier of C is non empty set
the carrier' of C is non empty set
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
(C) is non empty V7() V10( the carrier of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of (ConceptLattice C):]
[: the carrier of C, the carrier of (ConceptLattice C):] is non empty set
bool [: the carrier of C, the carrier of (ConceptLattice C):] is non empty set
(C) is non empty V7() V10( the carrier' of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier' of C) quasi_total Element of bool [: the carrier' of C, the carrier of (ConceptLattice C):]
[: the carrier' of C, the carrier of (ConceptLattice C):] is non empty set
bool [: the carrier' of C, the carrier of (ConceptLattice C):] is non empty set
f is Element of the carrier of C
(C) . f is Element of the carrier of (ConceptLattice C)
a is Element of the carrier' of C
(C) . a is Element of the carrier of (ConceptLattice C)
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
(C) is non empty V7() V10( the carrier of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of (ConceptLattice C):]
the carrier of C is non empty set
[: the carrier of C, the carrier of (ConceptLattice C):] is non empty set
bool [: the carrier of C, the carrier of (ConceptLattice C):] is non empty set
rng (C) is Element of bool the carrier of (ConceptLattice C)
bool the carrier of (ConceptLattice C) is non empty set
(C) is non empty V7() V10( the carrier' of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier' of C) quasi_total Element of bool [: the carrier' of C, the carrier of (ConceptLattice C):]
the carrier' of C is non empty set
[: the carrier' of C, the carrier of (ConceptLattice C):] is non empty set
bool [: the carrier' of C, the carrier of (ConceptLattice C):] is non empty set
rng (C) is Element of bool the carrier of (ConceptLattice C)
bool (rng (C)) is non empty set
a is Element of the carrier of (ConceptLattice C)
bool the carrier of C is non empty set
bool the carrier' of C is non empty set
a @ is strict non empty concept-like ConceptStr over C
the Extent of (a @) is Element of bool the carrier of C
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
{ ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ex b3 being Element of the carrier of C st
( b3 in the Extent of (a @) & b1 = (AttributeDerivation C) . ((ObjectDerivation C) . {b3}) & b2 = (ObjectDerivation C) . {b3} ) } is set
b is set
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
a is Element of the carrier of C
{a} is Element of bool the carrier of C
(ObjectDerivation C) . {a} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {a}) is Element of bool the carrier of C
a is Element of the carrier of C
{a} is Element of bool the carrier of C
(ObjectDerivation C) . {a} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {a}) is Element of bool the carrier of C
(C) . a is Element of the carrier of (ConceptLattice C)
b is Element of the carrier of (ConceptLattice C)
dom (C) is Element of bool the carrier of C
Av is Element of bool the carrier of C
v is Element of bool the carrier' of C
ConceptStr(# Av,v #) is strict ConceptStr over C
A is Element of the carrier of C
{A} is Element of bool the carrier of C
(ObjectDerivation C) . {A} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {A}) is Element of bool the carrier of C
"\/" ( { ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ex b3 being Element of the carrier of C st
( b3 in the Extent of (a @) & b1 = (AttributeDerivation C) . ((ObjectDerivation C) . {b3}) & b2 = (ObjectDerivation C) . {b3} ) } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
bool (rng (C)) is non empty set
a is Element of the carrier of (ConceptLattice C)
bool the carrier of C is non empty set
bool the carrier' of C is non empty set
a @ is strict non empty concept-like ConceptStr over C
the Intent of (a @) is Element of bool the carrier' of C
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
{ ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ex b3 being Element of the carrier' of C st
( b3 in the Intent of (a @) & b1 = (AttributeDerivation C) . {b3} & b2 = (ObjectDerivation C) . ((AttributeDerivation C) . {b3}) ) } is set
a is set
b is Element of bool the carrier of C
a is Element of bool the carrier' of C
ConceptStr(# b,a #) is strict ConceptStr over C
b is Element of the carrier' of C
{b} is Element of bool the carrier' of C
(AttributeDerivation C) . {b} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {b}) is Element of bool the carrier' of C
b is Element of the carrier' of C
{b} is Element of bool the carrier' of C
(AttributeDerivation C) . {b} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {b}) is Element of bool the carrier' of C
(C) . b is Element of the carrier of (ConceptLattice C)
Av is Element of the carrier of (ConceptLattice C)
dom (C) is Element of bool the carrier' of C
v is Element of bool the carrier of C
A is Element of bool the carrier' of C
ConceptStr(# v,A #) is strict ConceptStr over C
fb is Element of the carrier' of C
{fb} is Element of bool the carrier' of C
(AttributeDerivation C) . {fb} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {fb}) is Element of bool the carrier' of C
"/\" ( { ConceptStr(# b1,b2 #) where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ex b3 being Element of the carrier' of C st
( b3 in the Intent of (a @) & b1 = (AttributeDerivation C) . {b3} & b2 = (ObjectDerivation C) . ((AttributeDerivation C) . {b3}) ) } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
{ b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than { ConceptStr(# b1,b2 #) where b2 is Element of bool the carrier of C, b3 is Element of bool the carrier' of C : ex b4 being Element of the carrier' of C st
( b3 in the Intent of (a @) & b1 = (AttributeDerivation C) . {b3} & b2 = (ObjectDerivation C) . ((AttributeDerivation C) . {b3}) ) } } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice C) : b1 is_less_than { ConceptStr(# b1,b2 #) where b2 is Element of bool the carrier of C, b3 is Element of bool the carrier' of C : ex b4 being Element of the carrier' of C st
( b3 in the Intent of (a @) & b1 = (AttributeDerivation C) . {b3} & b2 = (ObjectDerivation C) . ((AttributeDerivation C) . {b3}) ) } } ,(ConceptLattice C)) is Element of the carrier of (ConceptLattice C)
C is non quasi-empty ContextStr
the carrier of C is non empty set
the carrier' of C is non empty set
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice C) is non empty set
(C) is non empty V7() V10( the carrier of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of (ConceptLattice C):]
[: the carrier of C, the carrier of (ConceptLattice C):] is non empty set
bool [: the carrier of C, the carrier of (ConceptLattice C):] is non empty set
(C) is non empty V7() V10( the carrier' of C) V11( the carrier of (ConceptLattice C)) Function-like V17( the carrier' of C) quasi_total Element of bool [: the carrier' of C, the carrier of (ConceptLattice C):]
[: the carrier' of C, the carrier of (ConceptLattice C):] is non empty set
bool [: the carrier' of C, the carrier of (ConceptLattice C):] is non empty set
f is Element of the carrier of C
(C) . f is Element of the carrier of (ConceptLattice C)
a is Element of the carrier' of C
(C) . a is Element of the carrier of (ConceptLattice C)
{a} is Element of bool the carrier' of C
bool the carrier' of C is non empty set
{f} is Element of bool the carrier of C
bool the carrier of C is non empty set
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
(ObjectDerivation C) . {f} is Element of bool the carrier' of C
(AttributeDerivation C) . ((ObjectDerivation C) . {f}) is Element of bool the carrier of C
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
{ b1 where b1 is Element of the carrier' of C : f is-connected-with b1 } is set
Av is Element of bool the carrier of C
v is Element of bool the carrier' of C
ConceptStr(# Av,v #) is strict ConceptStr over C
(AttributeDerivation C) . {a} is Element of bool the carrier of C
(ObjectDerivation C) . ((AttributeDerivation C) . {a}) is Element of bool the carrier' of C
A is Element of bool the carrier of C
fb is Element of bool the carrier' of C
ConceptStr(# A,fb #) is strict ConceptStr over C
((C) . a) @ is strict non empty concept-like ConceptStr over C
the Extent of (((C) . a) @) is Element of bool the carrier of C
((C) . f) @ is strict non empty concept-like ConceptStr over C
the Extent of (((C) . f) @) is Element of bool the carrier of C
Av is Element of bool the carrier of C
v is Element of bool the carrier' of C
ConceptStr(# Av,v #) is strict ConceptStr over C
(ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . {f})) is Element of bool the carrier' of C
A is Element of the carrier' of C
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of C is non empty set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of f is non empty set
[: the carrier of C, the carrier of f:] is non empty set
bool [: the carrier of C, the carrier of f:] is non empty set
a is non empty V7() V10( the carrier of C) V11( the carrier of f) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of f:]
b is set
proj1 a is set
a is set
a . b is set
a . a is set
dom a is Element of bool the carrier of C
bool the carrier of C is non empty set
a is Element of the carrier of C
b is Element of the carrier of C
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of C is non empty set
f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of f is non empty set
[: the carrier of C, the carrier of f:] is non empty set
bool [: the carrier of C, the carrier of f:] is non empty set
a is non empty V7() V10( the carrier of C) V11( the carrier of f) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of f:]
rng a is Element of bool the carrier of f
bool the carrier of f is non empty set
b is Element of the carrier of C
a is Element of the carrier of C
b "/\" a is Element of the carrier of C
a . (b "/\" a) is Element of the carrier of f
a . b is Element of the carrier of f
a . a is Element of the carrier of f
(a . b) "/\" (a . a) is Element of the carrier of f
{(a . b),(a . a)} is Element of bool the carrier of f
[: the carrier of f, the carrier of C:] is non empty set
bool [: the carrier of f, the carrier of C:] is non empty set
a " is V7() Function-like set
a is Element of the carrier of f
b is non empty V7() V10( the carrier of f) V11( the carrier of C) Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of C:]
b . a is Element of the carrier of C
a . (b . a) is Element of the carrier of f
{b,a} is Element of bool the carrier of C
bool the carrier of C is non empty set
b is Element of the carrier of C
"/\" ({b,a},C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than {b,a} } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than {b,a} } ,C) is Element of the carrier of C
b is Element of the carrier of f
"/\" ({(a . b),(a . a)},f) is Element of the carrier of f
{ b1 where b1 is Element of the carrier of f : b1 is_less_than {(a . b),(a . a)} } is set
"\/" ( { b1 where b1 is Element of the carrier of f : b1 is_less_than {(a . b),(a . a)} } ,f) is Element of the carrier of f
b is Element of the carrier of C
a is Element of the carrier of C
b "\/" a is Element of the carrier of C
a . (b "\/" a) is Element of the carrier of f
a . b is Element of the carrier of f
a . a is Element of the carrier of f
(a . b) "\/" (a . a) is Element of the carrier of f
{(a . b),(a . a)} is Element of bool the carrier of f
[: the carrier of f, the carrier of C:] is non empty set
bool [: the carrier of f, the carrier of C:] is non empty set
a " is V7() Function-like set
a is Element of the carrier of f
b is non empty V7() V10( the carrier of f) V11( the carrier of C) Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of C:]
b . a is Element of the carrier of C
a . (b . a) is Element of the carrier of f
{b,a} is Element of bool the carrier of C
bool the carrier of C is non empty set
b is Element of the carrier of C
"\/" ({b,a},C) is Element of the carrier of C
b is Element of the carrier of f
"\/" ({(a . b),(a . a)},f) is Element of the carrier of f
C is non quasi-empty ContextStr
the carrier of C is non empty set
bool the carrier of C is non empty set
the carrier' of C is non empty set
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool the carrier' of C is non empty set
bool (bool the carrier' of C) is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
f is ConceptStr over C
the Extent of f is Element of bool the carrier of C
(ObjectDerivation C) . the Extent of f is Element of bool the carrier' of C
the Intent of f is Element of bool the carrier' of C
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of C is non empty set
f is non quasi-empty ContextStr
ConceptLattice f is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of f is non empty set
[: the carrier of f, the carrier of C:] is non empty set
bool [: the carrier of f, the carrier of C:] is non empty set
the carrier' of f is non empty set
[: the carrier' of f, the carrier of C:] is non empty set
bool [: the carrier' of f, the carrier of C:] is non empty set
the carrier of (ConceptLattice f) is non empty set
a is non empty V7() V10( the carrier of (ConceptLattice f)) V11( the carrier of C) Function-like V17( the carrier of (ConceptLattice f)) quasi_total Homomorphism of ConceptLattice f,C
(f) is non empty V7() V10( the carrier of f) V11( the carrier of (ConceptLattice f)) Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of (ConceptLattice f):]
[: the carrier of f, the carrier of (ConceptLattice f):] is non empty set
bool [: the carrier of f, the carrier of (ConceptLattice f):] is non empty set
a * (f) is non empty V7() V10( the carrier of f) V11( the carrier of C) Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of C:]
(f) is non empty V7() V10( the carrier' of f) V11( the carrier of (ConceptLattice f)) Function-like V17( the carrier' of f) quasi_total Element of bool [: the carrier' of f, the carrier of (ConceptLattice f):]
[: the carrier' of f, the carrier of (ConceptLattice f):] is non empty set
bool [: the carrier' of f, the carrier of (ConceptLattice f):] is non empty set
a * (f) is non empty V7() V10( the carrier' of f) V11( the carrier of C) Function-like V17( the carrier' of f) quasi_total Element of bool [: the carrier' of f, the carrier of C:]
b is non empty V7() V10( the carrier of f) V11( the carrier of C) Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of C:]
rng b is Element of bool the carrier of C
bool the carrier of C is non empty set
bool (rng b) is non empty set
b is Element of the carrier of C
a is Element of the carrier of (ConceptLattice f)
a . a is Element of the carrier of C
rng (f) is Element of bool the carrier of (ConceptLattice f)
bool the carrier of (ConceptLattice f) is non empty set
bool (rng (f)) is non empty set
b is Element of bool (rng (f))
"\/" (b,(ConceptLattice f)) is Element of the carrier of (ConceptLattice f)
{ (a . b1) where b1 is Element of the carrier of (ConceptLattice f) : b1 in b } is set
v is Element of the carrier of C
A is Element of the carrier of (ConceptLattice f)
a . A is Element of the carrier of C
fb is Element of the carrier of (ConceptLattice f)
O9 is Element of the carrier of (ConceptLattice f)
a . O9 is Element of the carrier of C
a . fb is Element of the carrier of C
v is set
A is Element of the carrier of (ConceptLattice f)
a . A is Element of the carrier of C
dom (f) is Element of bool the carrier of f
bool the carrier of f is non empty set
fb is set
(f) . fb is set
dom a is Element of bool the carrier of (ConceptLattice f)
dom (a * (f)) is Element of bool the carrier of f
(a * (f)) . fb is set
v is Element of the carrier of C
A is Element of the carrier of (ConceptLattice f)
a . A is Element of the carrier of C
"\/" ( { (a . b1) where b1 is Element of the carrier of (ConceptLattice f) : b1 in b } ,C) is Element of the carrier of C
a is non empty V7() V10( the carrier' of f) V11( the carrier of C) Function-like V17( the carrier' of f) quasi_total Element of bool [: the carrier' of f, the carrier of C:]
rng a is Element of bool the carrier of C
bool (rng a) is non empty set
b is Element of the carrier of C
a is Element of the carrier of (ConceptLattice f)
a . a is Element of the carrier of C
rng (f) is Element of bool the carrier of (ConceptLattice f)
bool the carrier of (ConceptLattice f) is non empty set
bool (rng (f)) is non empty set
b is Element of bool (rng (f))
"/\" (b,(ConceptLattice f)) is Element of the carrier of (ConceptLattice f)
{ b1 where b1 is Element of the carrier of (ConceptLattice f) : b1 is_less_than b } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice f) : b1 is_less_than b } ,(ConceptLattice f)) is Element of the carrier of (ConceptLattice f)
{ (a . b1) where b1 is Element of the carrier of (ConceptLattice f) : b1 in b } is set
v is Element of the carrier of C
A is Element of the carrier of (ConceptLattice f)
a . A is Element of the carrier of C
fb is Element of the carrier of (ConceptLattice f)
O9 is Element of the carrier of (ConceptLattice f)
a . O9 is Element of the carrier of C
a . fb is Element of the carrier of C
v is set
A is Element of the carrier of (ConceptLattice f)
a . A is Element of the carrier of C
dom (f) is Element of bool the carrier' of f
bool the carrier' of f is non empty set
fb is set
(f) . fb is set
dom a is Element of bool the carrier of (ConceptLattice f)
dom (a * (f)) is Element of bool the carrier' of f
(a * (f)) . fb is set
v is Element of the carrier of C
A is Element of the carrier of (ConceptLattice f)
a . A is Element of the carrier of C
"/\" ( { (a . b1) where b1 is Element of the carrier of (ConceptLattice f) : b1 in b } ,C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than { (a . b1) where b2 is Element of the carrier of (ConceptLattice f) : b1 in b } } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than { (a . b1) where b2 is Element of the carrier of (ConceptLattice f) : b1 in b } } ,C) is Element of the carrier of C
b is Element of the carrier of f
a is Element of the carrier' of f
(f) . b is Element of the carrier of (ConceptLattice f)
(f) . a is Element of the carrier of (ConceptLattice f)
dom (f) is Element of bool the carrier' of f
bool the carrier' of f is non empty set
a . ((f) . a) is Element of the carrier of C
(a * (f)) . a is Element of the carrier of C
dom (f) is Element of bool the carrier of f
bool the carrier of f is non empty set
a . ((f) . b) is Element of the carrier of C
(a * (f)) . b is Element of the carrier of C
b . b is Element of the carrier of C
a . a is Element of the carrier of C
a is non empty V7() V10( the carrier of f) V11( the carrier of C) Function-like V17( the carrier of f) quasi_total Element of bool [: the carrier of f, the carrier of C:]
rng a is Element of bool the carrier of C
b is non empty V7() V10( the carrier' of f) V11( the carrier of C) Function-like V17( the carrier' of f) quasi_total Element of bool [: the carrier' of f, the carrier of C:]
rng b is Element of bool the carrier of C
{ [b1,ConceptStr(# b2,b3 #)] where b1 is Element of the carrier of C, b2 is Element of bool the carrier of f, b3 is Element of bool the carrier' of f : ( b2 = { b4 where b4 is Element of the carrier of f : a . b4 [= b1 } & b3 = { b4 where b4 is Element of the carrier' of f : b1 [= b . b4 } ) } is set
{ [ConceptStr(# b1,b2 #),b3] where b1 is Element of bool the carrier of f, b2 is Element of bool the carrier' of f, b3 is Element of the carrier of C : ( ConceptStr(# b1,b2 #) is non empty concept-like ConceptStr over f & b3 = "\/" ( { (a . b4) where b4 is Element of the carrier of f : b4 in b1 } ,C) ) } is set
B-carrier f is non empty Set-of-FormalConcepts of f
B-join f is non empty V7() V10([:(B-carrier f),(B-carrier f):]) V11( B-carrier f) Function-like V17([:(B-carrier f),(B-carrier f):]) quasi_total Element of bool [:[:(B-carrier f),(B-carrier f):],(B-carrier f):]
[:(B-carrier f),(B-carrier f):] is non empty set
[:[:(B-carrier f),(B-carrier f):],(B-carrier f):] is non empty set
bool [:[:(B-carrier f),(B-carrier f):],(B-carrier f):] is non empty set
B-meet f is non empty V7() V10([:(B-carrier f),(B-carrier f):]) V11( B-carrier f) Function-like V17([:(B-carrier f),(B-carrier f):]) quasi_total Element of bool [:[:(B-carrier f),(B-carrier f):],(B-carrier f):]
LattStr(# (B-carrier f),(B-join f),(B-meet f) #) is non empty strict LattStr
[: the carrier of (ConceptLattice f), the carrier of C:] is non empty set
a is set
b is Element of bool the carrier of f
Av is Element of bool the carrier' of f
ConceptStr(# b,Av #) is strict ConceptStr over f
v is Element of the carrier of C
[ConceptStr(# b,Av #),v] is V1() set
{ConceptStr(# b,Av #),v} is set
{ConceptStr(# b,Av #)} is set
{{ConceptStr(# b,Av #),v},{ConceptStr(# b,Av #)}} is set
{ (a . b1) where b1 is Element of the carrier of f : b1 in b } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in b } ,C) is Element of the carrier of C
[: the carrier of C, the carrier of (ConceptLattice f):] is non empty set
a is set
b is Element of the carrier of C
Av is Element of bool the carrier of f
v is Element of bool the carrier' of f
ConceptStr(# Av,v #) is strict ConceptStr over f
[b,ConceptStr(# Av,v #)] is V1() set
{b,ConceptStr(# Av,v #)} is set
{b} is set
{{b,ConceptStr(# Av,v #)},{b}} is set
{ b1 where b1 is Element of the carrier of f : a . b1 [= b } is set
{ b1 where b1 is Element of the carrier' of f : b [= b . b1 } is set
bool the carrier of f is non empty Element of bool (bool the carrier of f)
bool (bool the carrier of f) is non empty set
AttributeDerivation f is non empty V7() V10( bool the carrier' of f) V11( bool the carrier of f) Function-like V17( bool the carrier' of f) quasi_total Element of bool [:(bool the carrier' of f),(bool the carrier of f):]
bool the carrier' of f is non empty Element of bool (bool the carrier' of f)
bool (bool the carrier' of f) is non empty set
[:(bool the carrier' of f),(bool the carrier of f):] is non empty set
bool [:(bool the carrier' of f),(bool the carrier of f):] is non empty set
the Intent of ConceptStr(# Av,v #) is Element of bool the carrier' of f
(AttributeDerivation f) . the Intent of ConceptStr(# Av,v #) is Element of bool the carrier of f
the Extent of ConceptStr(# Av,v #) is Element of bool the carrier of f
A is set
{ (b . b1) where b1 is Element of the carrier' of f : b [= b . b1 } is set
"/\" ( { (b . b1) where b1 is Element of the carrier' of f : b [= b . b1 } ,C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than { (b . b1) where b2 is Element of the carrier' of f : b [= b . b1 } } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than { (b . b1) where b2 is Element of the carrier' of f : b [= b . b1 } } ,C) is Element of the carrier of C
bool (rng b) is non empty set
fb is Element of bool (rng b)
"/\" (fb,C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than fb } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than fb } ,C) is Element of the carrier of C
O9 is set
dom b is Element of bool the carrier' of f
A9 is set
b . A9 is set
fb is Element of the carrier' of f
b . fb is Element of the carrier of C
O9 is Element of the carrier of C
A9 is Element of the carrier' of f
b . A9 is Element of the carrier of C
{ b1 where b1 is Element of the carrier of f : for b2 being Element of the carrier' of f holds
( not b2 in the Intent of ConceptStr(# Av,v #) or b1 is-connected-with b2 ) } is set
fb is Element of the carrier of f
a . fb is Element of the carrier of C
O9 is Element of the carrier' of f
b . O9 is Element of the carrier of C
O9 is Element of the carrier of C
A9 is Element of the carrier' of f
b . A9 is Element of the carrier of C
A is set
fb is Element of the carrier of f
a . fb is Element of the carrier of C
O9 is Element of the carrier' of f
b . O9 is Element of the carrier of C
A9 is Element of the carrier' of f
b . A9 is Element of the carrier of C
O9 is Element of the carrier' of f
b . O9 is Element of the carrier of C
{ b1 where b1 is Element of the carrier of f : for b2 being Element of the carrier' of f holds
( not b2 in the Intent of ConceptStr(# Av,v #) or b1 is-connected-with b2 ) } is set
ObjectDerivation f is non empty V7() V10( bool the carrier of f) V11( bool the carrier' of f) Function-like V17( bool the carrier of f) quasi_total Element of bool [:(bool the carrier of f),(bool the carrier' of f):]
[:(bool the carrier of f),(bool the carrier' of f):] is non empty set
bool [:(bool the carrier of f),(bool the carrier' of f):] is non empty set
(ObjectDerivation f) . the Extent of ConceptStr(# Av,v #) is Element of bool the carrier' of f
A is set
{ (a . b1) where b1 is Element of the carrier of f : a . b1 [= b } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : a . b1 [= b } ,C) is Element of the carrier of C
bool (rng a) is non empty set
fb is Element of bool (rng a)
"\/" (fb,C) is Element of the carrier of C
O9 is set
dom a is Element of bool the carrier of f
A9 is set
a . A9 is set
fb is Element of the carrier of f
a . fb is Element of the carrier of C
O9 is Element of the carrier of C
A9 is Element of the carrier of f
a . A9 is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of f : for b2 being Element of the carrier of f holds
( not b2 in the Extent of ConceptStr(# Av,v #) or b2 is-connected-with b1 ) } is set
fb is Element of the carrier' of f
b . fb is Element of the carrier of C
O9 is Element of the carrier of f
a . O9 is Element of the carrier of C
O9 is Element of the carrier of C
A9 is Element of the carrier of f
a . A9 is Element of the carrier of C
A is set
fb is Element of the carrier' of f
b . fb is Element of the carrier of C
O9 is Element of the carrier of f
a . O9 is Element of the carrier of C
A9 is Element of the carrier of f
a . A9 is Element of the carrier of C
O9 is Element of the carrier of f
a . O9 is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of f : for b2 being Element of the carrier of f holds
( not b2 in the Extent of ConceptStr(# Av,v #) or b2 is-connected-with b1 ) } is set
bool [: the carrier of C, the carrier of (ConceptLattice f):] is non empty set
a is V7() V10( the carrier of C) V11( the carrier of (ConceptLattice f)) Element of bool [: the carrier of C, the carrier of (ConceptLattice f):]
b is set
Av is set
[b,Av] is V1() set
{b,Av} is set
{b} is set
{{b,Av},{b}} is set
v is set
[b,v] is V1() set
{b,v} is set
{{b,v},{b}} is set
A is Element of the carrier of C
fb is Element of bool the carrier of f
O9 is Element of bool the carrier' of f
ConceptStr(# fb,O9 #) is strict ConceptStr over f
[A,ConceptStr(# fb,O9 #)] is V1() set
{A,ConceptStr(# fb,O9 #)} is set
{A} is set
{{A,ConceptStr(# fb,O9 #)},{A}} is set
{ b1 where b1 is Element of the carrier of f : a . b1 [= A } is set
{ b1 where b1 is Element of the carrier' of f : A [= b . b1 } is set
A9 is Element of the carrier of C
fb is Element of bool the carrier of f
fa is Element of bool the carrier' of f
ConceptStr(# fb,fa #) is strict ConceptStr over f
[A9,ConceptStr(# fb,fa #)] is V1() set
{A9,ConceptStr(# fb,fa #)} is set
{A9} is set
{{A9,ConceptStr(# fb,fa #)},{A9}} is set
{ b1 where b1 is Element of the carrier of f : a . b1 [= A9 } is set
{ b1 where b1 is Element of the carrier' of f : A9 [= b . b1 } is set
[b,Av] `2 is set
[b,v] `2 is set
dom a is Element of bool the carrier of C
b is set
Av is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of f : Av [= b . b1 } is set
A is set
fb is Element of the carrier' of f
b . fb is Element of the carrier of C
{ b1 where b1 is Element of the carrier of f : a . b1 [= Av } is set
O9 is set
A9 is Element of the carrier of f
a . A9 is Element of the carrier of C
O9 is Element of bool the carrier of f
A is Element of bool the carrier' of f
ConceptStr(# O9,A #) is strict ConceptStr over f
[Av,ConceptStr(# O9,A #)] is V1() set
{Av,ConceptStr(# O9,A #)} is set
{Av} is set
{{Av,ConceptStr(# O9,A #)},{Av}} is set
bool [: the carrier of (ConceptLattice f), the carrier of C:] is non empty set
b is V7() V10( the carrier of (ConceptLattice f)) V11( the carrier of C) Element of bool [: the carrier of (ConceptLattice f), the carrier of C:]
dom b is Element of bool the carrier of (ConceptLattice f)
bool the carrier of (ConceptLattice f) is non empty set
Av is set
v is Element of bool the carrier of f
A is Element of bool the carrier' of f
ConceptStr(# v,A #) is strict ConceptStr over f
{ (a . b1) where b1 is Element of the carrier of f : b1 in v } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in v } ,C) is Element of the carrier of C
fb is Element of the carrier of C
[Av,fb] is V1() set
{Av,fb} is set
{Av} is set
{{Av,fb},{Av}} is set
v is set
A is set
[v,A] is V1() set
{v,A} is set
{v} is set
{{v,A},{v}} is set
fb is set
[v,fb] is V1() set
{v,fb} is set
{{v,fb},{v}} is set
O9 is Element of bool the carrier of f
A9 is Element of bool the carrier' of f
ConceptStr(# O9,A9 #) is strict ConceptStr over f
fb is Element of the carrier of C
[ConceptStr(# O9,A9 #),fb] is V1() set
{ConceptStr(# O9,A9 #),fb} is set
{ConceptStr(# O9,A9 #)} is set
{{ConceptStr(# O9,A9 #),fb},{ConceptStr(# O9,A9 #)}} is set
{ (a . b1) where b1 is Element of the carrier of f : b1 in O9 } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in O9 } ,C) is Element of the carrier of C
fa is Element of bool the carrier of f
fa is Element of bool the carrier' of f
ConceptStr(# fa,fa #) is strict ConceptStr over f
fb is Element of the carrier of C
[ConceptStr(# fa,fa #),fb] is V1() set
{ConceptStr(# fa,fa #),fb} is set
{ConceptStr(# fa,fa #)} is set
{{ConceptStr(# fa,fa #),fb},{ConceptStr(# fa,fa #)}} is set
{ (a . b1) where b1 is Element of the carrier of f : b1 in fa } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in fa } ,C) is Element of the carrier of C
[ConceptStr(# O9,A9 #),fb] `1 is set
[v,A] `1 is set
[v,fb] `1 is set
[ConceptStr(# fa,fa #),fb] `1 is set
[v,A] `2 is set
[v,fb] `2 is set
v is non empty V7() V10( the carrier of (ConceptLattice f)) V11( the carrier of C) Function-like V17( the carrier of (ConceptLattice f)) quasi_total Element of bool [: the carrier of (ConceptLattice f), the carrier of C:]
Av is non empty V7() V10( the carrier of C) V11( the carrier of (ConceptLattice f)) Function-like V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of (ConceptLattice f):]
A is Element of the carrier of C
Av . A is Element of the carrier of (ConceptLattice f)
v . (Av . A) is Element of the carrier of C
fb is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of f : fb [= b . b1 } is set
A9 is set
fb is Element of the carrier' of f
b . fb is Element of the carrier of C
{ b1 where b1 is Element of the carrier of f : a . b1 [= fb } is set
fa is set
fa is Element of the carrier of f
a . fa is Element of the carrier of C
fa is Element of bool the carrier of f
A9 is Element of bool the carrier' of f
ConceptStr(# fa,A9 #) is strict ConceptStr over f
the Extent of ConceptStr(# fa,A9 #) is Element of bool the carrier of f
{ (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of ConceptStr(# fa,A9 #) } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of ConceptStr(# fa,A9 #) } ,C) is Element of the carrier of C
{ (a . b1) where b1 is Element of the carrier of f : b1 in { b1 where b2 is Element of the carrier of f : a . b1 [= fb } } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in { b1 where b2 is Element of the carrier of f : a . b1 [= fb } } ,C) is Element of the carrier of C
bool (rng a) is non empty set
fb is Element of bool (rng a)
"\/" (fb,C) is Element of the carrier of C
Ab is set
dom a is Element of bool the carrier of f
xa is set
a . xa is set
Oa is Element of the carrier of f
a . Oa is Element of the carrier of C
Ab is Element of the carrier of C
xa is Element of the carrier of f
a . xa is Element of the carrier of C
Oa is Element of the carrier of f
a . Oa is Element of the carrier of C
[fb,ConceptStr(# fa,A9 #)] is V1() set
{fb,ConceptStr(# fa,A9 #)} is set
{fb} is set
{{fb,ConceptStr(# fa,A9 #)},{fb}} is set
rng Av is Element of bool the carrier of (ConceptLattice f)
[ConceptStr(# fa,A9 #),("\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of ConceptStr(# fa,A9 #) } ,C))] is V1() set
{ConceptStr(# fa,A9 #),("\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of ConceptStr(# fa,A9 #) } ,C))} is set
{ConceptStr(# fa,A9 #)} is set
{{ConceptStr(# fa,A9 #),("\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of ConceptStr(# fa,A9 #) } ,C))},{ConceptStr(# fa,A9 #)}} is set
v . ConceptStr(# fa,A9 #) is set
rng v is Element of bool the carrier of C
A is set
dom v is Element of bool the carrier of (ConceptLattice f)
dom Av is Element of bool the carrier of C
fb is set
[A,fb] is V1() set
{A,fb} is set
{A} is set
{{A,fb},{A}} is set
rng Av is Element of bool the carrier of (ConceptLattice f)
A9 is Element of the carrier of (ConceptLattice f)
v . A9 is Element of the carrier of C
O9 is Element of the carrier of C
Av . O9 is Element of the carrier of (ConceptLattice f)
v . (Av . O9) is Element of the carrier of C
A is Element of the carrier of (ConceptLattice f)
v . A is Element of the carrier of C
A @ is strict non empty concept-like ConceptStr over f
the Intent of (A @) is Element of bool the carrier' of f
{ (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } is set
"/\" ( { (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than { (b . b1) where b2 is Element of the carrier' of f : b1 in the Intent of (A @) } } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than { (b . b1) where b2 is Element of the carrier' of f : b1 in the Intent of (A @) } } ,C) is Element of the carrier of C
the Extent of (A @) is Element of bool the carrier of f
{ (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (A @) } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (A @) } ,C) is Element of the carrier of C
[(A @),("\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (A @) } ,C))] is V1() set
{(A @),("\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (A @) } ,C))} is set
{(A @)} is set
{{(A @),("\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (A @) } ,C))},{(A @)}} is set
{ (b . b1) where b1 is Element of the carrier' of f : "\/" ( { (a . b1) where b2 is Element of the carrier of f : b1 in the Extent of (A @) } ,C) [= b . b1 } is set
O9 is set
A9 is Element of the carrier' of f
b . A9 is Element of the carrier of C
fb is Element of the carrier of f
a . fb is Element of the carrier of C
fb is Element of the carrier of f
a . fb is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of f : for b2 being Element of the carrier of f holds
( not b2 in the Extent of (A @) or b2 is-connected-with b1 ) } is set
bool the carrier' of f is non empty Element of bool (bool the carrier' of f)
bool (bool the carrier' of f) is non empty set
ObjectDerivation f is non empty V7() V10( bool the carrier of f) V11( bool the carrier' of f) Function-like V17( bool the carrier of f) quasi_total Element of bool [:(bool the carrier of f),(bool the carrier' of f):]
bool the carrier of f is non empty Element of bool (bool the carrier of f)
bool (bool the carrier of f) is non empty set
[:(bool the carrier of f),(bool the carrier' of f):] is non empty set
bool [:(bool the carrier of f),(bool the carrier' of f):] is non empty set
(ObjectDerivation f) . the Extent of (A @) is Element of bool the carrier' of f
O9 is Element of the carrier of f
a . O9 is Element of the carrier of C
A9 is Element of the carrier' of f
b . A9 is Element of the carrier of C
bool the carrier' of f is non empty Element of bool (bool the carrier' of f)
bool (bool the carrier' of f) is non empty set
ObjectDerivation f is non empty V7() V10( bool the carrier of f) V11( bool the carrier' of f) Function-like V17( bool the carrier of f) quasi_total Element of bool [:(bool the carrier of f),(bool the carrier' of f):]
bool the carrier of f is non empty Element of bool (bool the carrier of f)
bool (bool the carrier of f) is non empty set
[:(bool the carrier of f),(bool the carrier' of f):] is non empty set
bool [:(bool the carrier of f),(bool the carrier' of f):] is non empty set
(ObjectDerivation f) . the Extent of (A @) is Element of bool the carrier' of f
{ b1 where b1 is Element of the carrier' of f : for b2 being Element of the carrier of f holds
( not b2 in the Extent of (A @) or b2 is-connected-with b1 ) } is set
fb is Element of the carrier' of f
O9 is set
A9 is Element of the carrier' of f
b . A9 is Element of the carrier of C
fb is Element of the carrier of C
fa is Element of the carrier of f
a . fa is Element of the carrier of C
"/\" ( { (b . b1) where b1 is Element of the carrier' of f : "\/" ( { (a . b1) where b2 is Element of the carrier of f : b1 in the Extent of (A @) } ,C) [= b . b1 } ,C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than { (b . b1) where b2 is Element of the carrier' of f : "\/" ( { (a . b1) where b3 is Element of the carrier of f : b1 in the Extent of (A @) } ,C) [= b . b1 } } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than { (b . b1) where b2 is Element of the carrier' of f : "\/" ( { (a . b1) where b3 is Element of the carrier of f : b1 in the Extent of (A @) } ,C) [= b . b1 } } ,C) is Element of the carrier of C
bool (rng b) is non empty set
O9 is Element of bool (rng b)
"/\" (O9,C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than O9 } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than O9 } ,C) is Element of the carrier of C
A9 is set
dom b is Element of bool the carrier' of f
fb is set
b . fb is set
fa is Element of the carrier' of f
b . fa is Element of the carrier of C
A9 is Element of the carrier of C
fb is Element of the carrier' of f
b . fb is Element of the carrier of C
v . (A @) is set
A is Element of the carrier of (ConceptLattice f)
v . A is Element of the carrier of C
Av . (v . A) is Element of the carrier of (ConceptLattice f)
A @ is strict non empty concept-like ConceptStr over f
the Intent of (A @) is Element of bool the carrier' of f
{ (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } is set
"/\" ( { (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than { (b . b1) where b2 is Element of the carrier' of f : b1 in the Intent of (A @) } } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than { (b . b1) where b2 is Element of the carrier' of f : b1 in the Intent of (A @) } } ,C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of f : "/\" ( { (b . b1) where b2 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C) [= b . b1 } is set
A9 is set
fb is Element of the carrier' of f
b . fb is Element of the carrier of C
{ b1 where b1 is Element of the carrier of f : a . b1 [= "/\" ( { (b . b1) where b2 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C) } is set
fa is set
fa is Element of the carrier of f
a . fa is Element of the carrier of C
fa is Element of bool the carrier of f
{ b1 where b1 is Element of the carrier of f : for b2 being Element of the carrier' of f holds
( not b2 in the Intent of (A @) or a . b1 [= b . b2 ) } is set
fa is set
fb is Element of the carrier of f
a . fb is Element of the carrier of C
Ab is Element of the carrier' of f
b . Ab is Element of the carrier of C
fa is set
fb is Element of the carrier of f
a . fb is Element of the carrier of C
Ab is Element of the carrier of C
xa is Element of the carrier' of f
b . xa is Element of the carrier of C
{ b1 where b1 is Element of the carrier of f : for b2 being Element of the carrier' of f holds
( not b2 in the Intent of (A @) or b1 is-connected-with b2 ) } is set
fa is set
fb is Element of the carrier of f
a . fb is Element of the carrier of C
Ab is Element of the carrier' of f
b . Ab is Element of the carrier of C
fa is set
fb is Element of the carrier of f
a . fb is Element of the carrier of C
Ab is Element of the carrier' of f
b . Ab is Element of the carrier of C
bool the carrier of f is non empty Element of bool (bool the carrier of f)
bool (bool the carrier of f) is non empty set
AttributeDerivation f is non empty V7() V10( bool the carrier' of f) V11( bool the carrier of f) Function-like V17( bool the carrier' of f) quasi_total Element of bool [:(bool the carrier' of f),(bool the carrier of f):]
bool the carrier' of f is non empty Element of bool (bool the carrier' of f)
bool (bool the carrier' of f) is non empty set
[:(bool the carrier' of f),(bool the carrier of f):] is non empty set
bool [:(bool the carrier' of f),(bool the carrier of f):] is non empty set
(AttributeDerivation f) . the Intent of (A @) is Element of bool the carrier of f
the Extent of (A @) is Element of bool the carrier of f
Av . ("/\" ( { (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C)) is Element of the carrier of (ConceptLattice f)
A9 is Element of bool the carrier' of f
ConceptStr(# fa,A9 #) is strict ConceptStr over f
[("/\" ( { (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C)),ConceptStr(# fa,A9 #)] is V1() set
{("/\" ( { (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C)),ConceptStr(# fa,A9 #)} is set
{("/\" ( { (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C))} is set
{{("/\" ( { (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C)),ConceptStr(# fa,A9 #)},{("/\" ( { (b . b1) where b1 is Element of the carrier' of f : b1 in the Intent of (A @) } ,C))}} is set
ObjectDerivation f is non empty V7() V10( bool the carrier of f) V11( bool the carrier' of f) Function-like V17( bool the carrier of f) quasi_total Element of bool [:(bool the carrier of f),(bool the carrier' of f):]
[:(bool the carrier of f),(bool the carrier' of f):] is non empty set
bool [:(bool the carrier of f),(bool the carrier' of f):] is non empty set
(ObjectDerivation f) . the Extent of (A @) is Element of bool the carrier' of f
A is Element of the carrier of C
fb is Element of the carrier of C
Av . A is Element of the carrier of (ConceptLattice f)
Av . fb is Element of the carrier of (ConceptLattice f)
{ b1 where b1 is Element of the carrier of f : a . b1 [= A } is set
{ b1 where b1 is Element of the carrier of f : a . b1 [= fb } is set
fb is set
fa is Element of the carrier of f
a . fa is Element of the carrier of C
dom Av is Element of bool the carrier of C
fb is set
[A,fb] is V1() set
{A,fb} is set
{A} is set
{{A,fb},{A}} is set
fa is set
[fb,fa] is V1() set
{fb,fa} is set
{fb} is set
{{fb,fa},{fb}} is set
fa is Element of the carrier of C
fb is Element of bool the carrier of f
Ab is Element of bool the carrier' of f
ConceptStr(# fb,Ab #) is strict ConceptStr over f
[fa,ConceptStr(# fb,Ab #)] is V1() set
{fa,ConceptStr(# fb,Ab #)} is set
{fa} is set
{{fa,ConceptStr(# fb,Ab #)},{fa}} is set
{ b1 where b1 is Element of the carrier of f : a . b1 [= fa } is set
{ b1 where b1 is Element of the carrier' of f : fa [= b . b1 } is set
[fb,fa] `1 is set
[fa,ConceptStr(# fb,Ab #)] `1 is set
(Av . fb) @ is strict non empty concept-like ConceptStr over f
the Extent of ((Av . fb) @) is Element of bool the carrier of f
xa is Element of the carrier of C
Oa is Element of bool the carrier of f
Aa is Element of bool the carrier' of f
ConceptStr(# Oa,Aa #) is strict ConceptStr over f
[xa,ConceptStr(# Oa,Aa #)] is V1() set
{xa,ConceptStr(# Oa,Aa #)} is set
{xa} is set
{{xa,ConceptStr(# Oa,Aa #)},{xa}} is set
{ b1 where b1 is Element of the carrier of f : a . b1 [= xa } is set
{ b1 where b1 is Element of the carrier' of f : xa [= b . b1 } is set
[A,fb] `1 is set
[xa,ConceptStr(# Oa,Aa #)] `1 is set
(Av . A) @ is strict non empty concept-like ConceptStr over f
the Extent of ((Av . A) @) is Element of bool the carrier of f
A is Element of the carrier of (ConceptLattice f)
v . A is Element of the carrier of C
fb is Element of the carrier of (ConceptLattice f)
v . fb is Element of the carrier of C
Av . (v . A) is Element of the carrier of (ConceptLattice f)
Av . (v . fb) is Element of the carrier of (ConceptLattice f)
A is Element of the carrier of (ConceptLattice f)
fb is Element of the carrier of (ConceptLattice f)
v . A is Element of the carrier of C
v . fb is Element of the carrier of C
A @ is strict non empty concept-like ConceptStr over f
the Extent of (A @) is Element of bool the carrier of f
{ (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (A @) } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (A @) } ,C) is Element of the carrier of C
fb @ is strict non empty concept-like ConceptStr over f
the Extent of (fb @) is Element of bool the carrier of f
{ (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (fb @) } is set
"\/" ( { (a . b1) where b1 is Element of the carrier of f : b1 in the Extent of (fb @) } ,C) is Element of the carrier of C
O9 is Element of the carrier of C
[(A @),O9] is V1() set
{(A @),O9} is set
{(A @)} is set
{{(A @),O9},{(A @)}} is set
v . (A @) is set
A9 is Element of the carrier of C
[(fb @),A9] is V1() set
{(fb @),A9} is set
{(fb @)} is set
{{(fb @),A9},{(fb @)}} is set
v . (fb @) is set
fb is set
fa is Element of the carrier of f
a . fa is Element of the carrier of C
A is non empty V7() V10( the carrier of (ConceptLattice f)) V11( the carrier of C) Function-like V17( the carrier of (ConceptLattice f)) quasi_total Homomorphism of ConceptLattice f,C
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of C is non empty set
LattRel C is V7() V10( the carrier of C) V11( the carrier of C) V17( the carrier of C) quasi_total V89() V92() V96() Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
ContextStr(# the carrier of C, the carrier of C,(LattRel C) #) is strict ContextStr
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
(C) is non quasi-empty strict ContextStr
the carrier of C is non empty set
LattRel C is V7() V10( the carrier of C) V11( the carrier of C) V17( the carrier of C) quasi_total V89() V92() V96() Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
ContextStr(# the carrier of C, the carrier of C,(LattRel C) #) is strict ContextStr
ConceptLattice (C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (C) is non empty set
[: the carrier of (C), the carrier of C:] is non empty set
bool [: the carrier of (C), the carrier of C:] is non empty set
id the carrier of C is non empty V7() V10( the carrier of C) V11( the carrier of C) Function-like one-to-one V17( the carrier of C) quasi_total Element of bool [: the carrier of C, the carrier of C:]
the carrier' of (C) is non empty set
[: the carrier' of (C), the carrier of C:] is non empty set
bool [: the carrier' of (C), the carrier of C:] is non empty set
f is non empty V7() V10( the carrier of (C)) V11( the carrier of C) Function-like V17( the carrier of (C)) quasi_total Element of bool [: the carrier of (C), the carrier of C:]
a is non empty V7() V10( the carrier' of (C)) V11( the carrier of C) Function-like V17( the carrier' of (C)) quasi_total Element of bool [: the carrier' of (C), the carrier of C:]
b is Element of the carrier of (C)
f . b is Element of the carrier of C
a is Element of the carrier' of (C)
a . a is Element of the carrier of C
b is Element of the carrier of C
a is Element of the carrier of C
[b,a] is V1() Element of [: the carrier of (C), the carrier' of (C):]
[: the carrier of (C), the carrier' of (C):] is non empty set
{b,a} is set
{b} is set
{{b,a},{b}} is set
the Information of (C) is V7() V10( the carrier of (C)) V11( the carrier' of (C)) Element of bool [: the carrier of (C), the carrier' of (C):]
bool [: the carrier of (C), the carrier' of (C):] is non empty set
rng a is Element of bool the carrier of C
bool the carrier of C is non empty set
bool (rng a) is non empty set
b is Element of the carrier of C
{b} is Element of bool the carrier of C
"/\" ({b},C) is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : b1 is_less_than {b} } is set
"\/" ( { b1 where b1 is Element of the carrier of C : b1 is_less_than {b} } ,C) is Element of the carrier of C
rng f is Element of bool the carrier of C
bool (rng f) is non empty set
b is Element of the carrier of C
{b} is Element of bool the carrier of C
"\/" ({b},C) is Element of the carrier of C
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(C) is non quasi-empty strict ContextStr
the carrier of C is non empty set
LattRel C is V7() V10( the carrier of C) V11( the carrier of C) V17( the carrier of C) quasi_total V89() V92() V96() Element of bool [: the carrier of C, the carrier of C:]
[: the carrier of C, the carrier of C:] is non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
ContextStr(# the carrier of C, the carrier of C,(LattRel C) #) is strict ContextStr
ConceptLattice (C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
f is non quasi-empty ContextStr
ConceptLattice f is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
bool the carrier of C is non empty set
a is Element of bool the carrier of C
the carrier of (ConceptLattice f) is non empty set
b is non empty V7() V10( the carrier of C) V11( the carrier of (ConceptLattice f)) Function-like V17( the carrier of C) quasi_total Homomorphism of C, ConceptLattice f
{ (b . b1) where b1 is Element of the carrier of C : b1 in a } is set
b is set
a is Element of the carrier of C
b . a is Element of the carrier of (ConceptLattice f)
bool the carrier of (ConceptLattice f) is non empty set
b is Element of bool the carrier of (ConceptLattice f)
"/\" (b,(ConceptLattice f)) is Element of the carrier of (ConceptLattice f)
{ b1 where b1 is Element of the carrier of (ConceptLattice f) : b1 is_less_than b } is set
"\/" ( { b1 where b1 is Element of the carrier of (ConceptLattice f) : b1 is_less_than b } ,(ConceptLattice f)) is Element of the carrier of (ConceptLattice f)
b is Element of the carrier of C
b . b is Element of the carrier of (ConceptLattice f)
Av is Element of the carrier of C
b . Av is Element of the carrier of (ConceptLattice f)
v is Element of the carrier of (ConceptLattice f)
A is Element of the carrier of C
b . A is Element of the carrier of (ConceptLattice f)
Av is Element of the carrier of C
b . Av is Element of the carrier of (ConceptLattice f)
C is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
C .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (C .:) is non empty set
bool the carrier of (C .:) is non empty set
f is Element of bool the carrier of (C .:)
the carrier of C is non empty set
the L_meet of C is non empty V7() V10([: the carrier of C, the carrier of C:]) V11( the carrier of C) Function-like V17([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is non empty set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is non empty set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is non empty set
the L_join of C is non empty V7() V10([: the carrier of C, the carrier of C:]) V11( the carrier of C) Function-like V17([: the carrier of C, the carrier of C:]) quasi_total Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
LattStr(# the carrier of C, the L_meet of C, the L_join of C #) is non empty strict LattStr
bool the carrier of C is non empty set
a is Element of bool the carrier of C
"\/" (a,C) is Element of the carrier of C
LattRel (C .:) is V7() V10( the carrier of (C .:)) V11( the carrier of (C .:)) V17( the carrier of (C .:)) quasi_total V89() V92() V96() Element of bool [: the carrier of (C .:), the carrier of (C .:):]
[: the carrier of (C .:), the carrier of (C .:):] is non empty set
bool [: the carrier of (C .:), the carrier of (C .:):] is non empty set
LattRel C is V7() V10( the carrier of C) V11( the carrier of C) V17( the carrier of C) quasi_total V89() V92() V96() Element of bool [: the carrier of C, the carrier of C:]
bool [: the carrier of C, the carrier of C:] is non empty set
(LattRel C) ~ is V7() V10( the carrier of C) V11( the carrier of C) V17( the carrier of C) quasi_total V89() V92() V96() Element of bool [: the carrier of C, the carrier of C:]
(C .:) .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
LattRel ((C .:) .:) is V7() V10( the carrier of ((C .:) .:)) V11( the carrier of ((C .:) .:)) V17( the carrier of ((C .:) .:)) quasi_total V89() V92() V96() Element of bool [: the carrier of ((C .:) .:), the carrier of ((C .:) .:):]
the carrier of ((C .:) .:) is non empty set
[: the carrier of ((C .:) .:), the carrier of ((C .:) .:):] is non empty set
bool [: the carrier of ((C .:) .:), the carrier of ((C .:) .:):] is non empty set
((LattRel C) ~) ~ is V7() V10( the carrier of C) V11( the carrier of C) V17( the carrier of C) quasi_total V89() V92() V96() Element of bool [: the carrier of C, the carrier of C:]
a is Element of the carrier of (C .:)
b is Element of the carrier of (C .:)
a is Element of the carrier of C
b is Element of the carrier of C
Av is Element of the carrier of (C .:)
LattPOSet (C .:) is non empty strict V82() V83() V84() RelStr
RelStr(# the carrier of (C .:),(LattRel (C .:)) #) is strict RelStr
b % is Element of the carrier of (LattPOSet (C .:))
the carrier of (LattPOSet (C .:)) is non empty set
Av % is Element of the carrier of (LattPOSet (C .:))
[(b %),(Av %)] is V1() Element of [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):]
[: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):] is non empty set
{(b %),(Av %)} is set
{(b %)} is set
{{(b %),(Av %)},{(b %)}} is set
the InternalRel of (LattPOSet (C .:)) is V7() V10( the carrier of (LattPOSet (C .:))) V11( the carrier of (LattPOSet (C .:))) Element of bool [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):]
bool [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):] is non empty set
[(Av %),(b %)] is V1() Element of [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):]
{(Av %),(b %)} is set
{(Av %)} is set
{{(Av %),(b %)},{(Av %)}} is set
the InternalRel of (LattPOSet (C .:)) ~ is V7() V10( the carrier of (LattPOSet (C .:))) V11( the carrier of (LattPOSet (C .:))) Element of bool [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):]
LattPOSet ((C .:) .:) is non empty strict V82() V83() V84() RelStr
RelStr(# the carrier of ((C .:) .:),(LattRel ((C .:) .:)) #) is strict RelStr
the InternalRel of (LattPOSet ((C .:) .:)) is V7() V10( the carrier of (LattPOSet ((C .:) .:))) V11( the carrier of (LattPOSet ((C .:) .:))) Element of bool [: the carrier of (LattPOSet ((C .:) .:)), the carrier of (LattPOSet ((C .:) .:)):]
the carrier of (LattPOSet ((C .:) .:)) is non empty set
[: the carrier of (LattPOSet ((C .:) .:)), the carrier of (LattPOSet ((C .:) .:)):] is non empty set
bool [: the carrier of (LattPOSet ((C .:) .:)), the carrier of (LattPOSet ((C .:) .:)):] is non empty set
LattPOSet C is non empty strict V82() V83() V84() RelStr
RelStr(# the carrier of C,(LattRel C) #) is strict RelStr
b % is Element of the carrier of (LattPOSet C)
the carrier of (LattPOSet C) is non empty set
a % is Element of the carrier of (LattPOSet C)
LattPOSet C is non empty strict V82() V83() V84() RelStr
RelStr(# the carrier of C,(LattRel C) #) is strict RelStr
("\/" (a,C)) % is Element of the carrier of (LattPOSet C)
the carrier of (LattPOSet C) is non empty set
a % is Element of the carrier of (LattPOSet C)
[(("\/" (a,C)) %),(a %)] is V1() Element of [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):]
[: the carrier of (LattPOSet C), the carrier of (LattPOSet C):] is non empty set
{(("\/" (a,C)) %),(a %)} is set
{(("\/" (a,C)) %)} is set
{{(("\/" (a,C)) %),(a %)},{(("\/" (a,C)) %)}} is set
the InternalRel of (LattPOSet C) is V7() V10( the carrier of (LattPOSet C)) V11( the carrier of (LattPOSet C)) Element of bool [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):]
bool [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):] is non empty set
[(a %),(("\/" (a,C)) %)] is V1() Element of [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):]
{(a %),(("\/" (a,C)) %)} is set
{(a %)} is set
{{(a %),(("\/" (a,C)) %)},{(a %)}} is set
the InternalRel of (LattPOSet C) ~ is V7() V10( the carrier of (LattPOSet C)) V11( the carrier of (LattPOSet C)) Element of bool [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):]
LattPOSet (C .:) is non empty strict V82() V83() V84() RelStr
RelStr(# the carrier of (C .:),(LattRel (C .:)) #) is strict RelStr
the InternalRel of (LattPOSet (C .:)) is V7() V10( the carrier of (LattPOSet (C .:))) V11( the carrier of (LattPOSet (C .:))) Element of bool [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):]
the carrier of (LattPOSet (C .:)) is non empty set
[: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):] is non empty set
bool [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):] is non empty set
b % is Element of the carrier of (LattPOSet (C .:))
a % is Element of the carrier of (LattPOSet (C .:))
b is Element of the carrier of (C .:)
a is Element of the carrier of C
LattPOSet C is non empty strict V82() V83() V84() RelStr
RelStr(# the carrier of C,(LattRel C) #) is strict RelStr
a % is Element of the carrier of (LattPOSet C)
the carrier of (LattPOSet C) is non empty set
("\/" (a,C)) % is Element of the carrier of (LattPOSet C)
[(a %),(("\/" (a,C)) %)] is V1() Element of [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):]
[: the carrier of (LattPOSet C), the carrier of (LattPOSet C):] is non empty set
{(a %),(("\/" (a,C)) %)} is set
{(a %)} is set
{{(a %),(("\/" (a,C)) %)},{(a %)}} is set
the InternalRel of (LattPOSet C) is V7() V10( the carrier of (LattPOSet C)) V11( the carrier of (LattPOSet C)) Element of bool [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):]
bool [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):] is non empty set
[(("\/" (a,C)) %),(a %)] is V1() Element of [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):]
{(("\/" (a,C)) %),(a %)} is set
{(("\/" (a,C)) %)} is set
{{(("\/" (a,C)) %),(a %)},{(("\/" (a,C)) %)}} is set
the InternalRel of (LattPOSet C) ~ is V7() V10( the carrier of (LattPOSet C)) V11( the carrier of (LattPOSet C)) Element of bool [: the carrier of (LattPOSet C), the carrier of (LattPOSet C):]
LattPOSet (C .:) is non empty strict V82() V83() V84() RelStr
RelStr(# the carrier of (C .:),(LattRel (C .:)) #) is strict RelStr
the InternalRel of (LattPOSet (C .:)) is V7() V10( the carrier of (LattPOSet (C .:))) V11( the carrier of (LattPOSet (C .:))) Element of bool [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):]
the carrier of (LattPOSet (C .:)) is non empty set
[: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):] is non empty set
bool [: the carrier of (LattPOSet (C .:)), the carrier of (LattPOSet (C .:)):] is non empty set
a % is Element of the carrier of (LattPOSet (C .:))
b % is Element of the carrier of (LattPOSet (C .:))
C is non quasi-empty ContextStr
the carrier' of C is non empty set
the carrier of C is non empty set
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
C is non quasi-empty strict ContextStr
(C) is non quasi-empty strict ContextStr
the carrier' of C is non empty set
the carrier of C is non empty set
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
((C)) is non quasi-empty strict ContextStr
the carrier' of (C) is non empty set
the carrier of (C) is non empty set
the Information of (C) is V7() V10( the carrier of (C)) V11( the carrier' of (C)) Element of bool [: the carrier of (C), the carrier' of (C):]
[: the carrier of (C), the carrier' of (C):] is non empty set
bool [: the carrier of (C), the carrier' of (C):] is non empty set
the Information of (C) ~ is V7() V10( the carrier' of (C)) V11( the carrier of (C)) Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is non empty set
bool [: the carrier' of (C), the carrier of (C):] is non empty set
ContextStr(# the carrier' of (C), the carrier of (C),( the Information of (C) ~) #) is strict ContextStr
C is non quasi-empty ContextStr
the carrier of C is non empty set
bool the carrier of C is non empty set
the carrier' of C is non empty set
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool the carrier' of C is non empty set
bool (bool the carrier' of C) is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
(C) is non quasi-empty strict ContextStr
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
AttributeDerivation (C) is non empty V7() V10( bool the carrier' of (C)) V11( bool the carrier of (C)) Function-like V17( bool the carrier' of (C)) quasi_total Element of bool [:(bool the carrier' of (C)),(bool the carrier of (C)):]
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty Element of bool (bool the carrier' of (C))
bool the carrier' of (C) is non empty set
bool (bool the carrier' of (C)) is non empty set
the carrier of (C) is non empty set
bool the carrier of (C) is non empty Element of bool (bool the carrier of (C))
bool the carrier of (C) is non empty set
bool (bool the carrier of (C)) is non empty set
[:(bool the carrier' of (C)),(bool the carrier of (C)):] is non empty set
bool [:(bool the carrier' of (C)),(bool the carrier of (C)):] is non empty set
f is Element of bool the carrier of C
(ObjectDerivation C) . f is Element of bool the carrier' of C
(AttributeDerivation (C)) . f is set
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in f or b2 is-connected-with b1 ) } is set
a is Element of bool the carrier' of (C)
{ b1 where b1 is Element of the carrier of (C) : for b2 being Element of the carrier' of (C) holds
( not b2 in a or b1 is-connected-with b2 ) } is set
b is set
a is Element of the carrier' of C
b is Element of the carrier of (C)
Av is Element of the carrier' of (C)
v is Element of the carrier of C
[v,a] is V1() Element of [: the carrier of C, the carrier' of C:]
{v,a} is set
{v} is set
{{v,a},{v}} is set
[a,v] is V1() Element of [: the carrier' of C, the carrier of C:]
{a,v} is set
{a} is set
{{a,v},{a}} is set
the Information of (C) is V7() V10( the carrier of (C)) V11( the carrier' of (C)) Element of bool [: the carrier of (C), the carrier' of (C):]
[: the carrier of (C), the carrier' of (C):] is non empty set
bool [: the carrier of (C), the carrier' of (C):] is non empty set
b is set
a is Element of the carrier of (C)
b is Element of the carrier' of C
Av is Element of the carrier of C
v is Element of the carrier' of (C)
[a,v] is V1() Element of [: the carrier of (C), the carrier' of (C):]
[: the carrier of (C), the carrier' of (C):] is non empty set
{a,v} is set
{a} is set
{{a,v},{a}} is set
the Information of (C) is V7() V10( the carrier of (C)) V11( the carrier' of (C)) Element of bool [: the carrier of (C), the carrier' of (C):]
bool [: the carrier of (C), the carrier' of (C):] is non empty set
[Av,b] is V1() Element of [: the carrier of C, the carrier' of C:]
{Av,b} is set
{Av} is set
{{Av,b},{Av}} is set
(AttributeDerivation (C)) . a is Element of bool the carrier of (C)
C is non quasi-empty ContextStr
the carrier' of C is non empty set
bool the carrier' of C is non empty set
the carrier of C is non empty set
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
(C) is non quasi-empty strict ContextStr
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
ObjectDerivation (C) is non empty V7() V10( bool the carrier of (C)) V11( bool the carrier' of (C)) Function-like V17( bool the carrier of (C)) quasi_total Element of bool [:(bool the carrier of (C)),(bool the carrier' of (C)):]
the carrier of (C) is non empty set
bool the carrier of (C) is non empty Element of bool (bool the carrier of (C))
bool the carrier of (C) is non empty set
bool (bool the carrier of (C)) is non empty set
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty Element of bool (bool the carrier' of (C))
bool the carrier' of (C) is non empty set
bool (bool the carrier' of (C)) is non empty set
[:(bool the carrier of (C)),(bool the carrier' of (C)):] is non empty set
bool [:(bool the carrier of (C)),(bool the carrier' of (C)):] is non empty set
f is Element of bool the carrier' of C
(AttributeDerivation C) . f is Element of bool the carrier of C
(ObjectDerivation (C)) . f is set
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in f or b1 is-connected-with b2 ) } is set
a is Element of bool the carrier of (C)
{ b1 where b1 is Element of the carrier' of (C) : for b2 being Element of the carrier of (C) holds
( not b2 in a or b2 is-connected-with b1 ) } is set
b is set
a is Element of the carrier of C
b is Element of the carrier' of (C)
Av is Element of the carrier of (C)
v is Element of the carrier' of C
[a,v] is V1() Element of [: the carrier of C, the carrier' of C:]
{a,v} is set
{a} is set
{{a,v},{a}} is set
[Av,b] is V1() Element of [: the carrier of (C), the carrier' of (C):]
[: the carrier of (C), the carrier' of (C):] is non empty set
{Av,b} is set
{Av} is set
{{Av,b},{Av}} is set
the Information of (C) is V7() V10( the carrier of (C)) V11( the carrier' of (C)) Element of bool [: the carrier of (C), the carrier' of (C):]
bool [: the carrier of (C), the carrier' of (C):] is non empty set
b is set
a is Element of the carrier' of (C)
b is Element of the carrier of C
Av is Element of the carrier' of C
v is Element of the carrier of (C)
[v,a] is V1() Element of [: the carrier of (C), the carrier' of (C):]
[: the carrier of (C), the carrier' of (C):] is non empty set
{v,a} is set
{v} is set
{{v,a},{v}} is set
the Information of (C) is V7() V10( the carrier of (C)) V11( the carrier' of (C)) Element of bool [: the carrier of (C), the carrier' of (C):]
bool [: the carrier of (C), the carrier' of (C):] is non empty set
[b,Av] is V1() Element of [: the carrier of C, the carrier' of C:]
{b,Av} is set
{b} is set
{{b,Av},{b}} is set
(ObjectDerivation (C)) . a is Element of bool the carrier' of (C)
C is non quasi-empty ContextStr
(C) is non quasi-empty strict ContextStr
the carrier' of C is non empty set
the carrier of C is non empty set
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
f is ConceptStr over C
the Intent of f is Element of bool the carrier' of C
bool the carrier' of C is non empty set
the Extent of f is Element of bool the carrier of C
bool the carrier of C is non empty set
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
a is Element of bool the carrier of (C)
b is Element of bool the carrier' of (C)
ConceptStr(# a,b #) is strict ConceptStr over (C)
the Extent of ConceptStr(# a,b #) is Element of bool the carrier of (C)
the Intent of ConceptStr(# a,b #) is Element of bool the carrier' of (C)
a is strict ConceptStr over (C)
the Extent of a is Element of bool the carrier of (C)
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
the Intent of a is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
b is strict ConceptStr over (C)
the Extent of b is Element of bool the carrier of (C)
the Intent of b is Element of bool the carrier' of (C)
C is non quasi-empty ContextStr
(C) is non quasi-empty strict ContextStr
the carrier' of C is non empty set
the carrier of C is non empty set
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
f is non empty concept-like ConceptStr over C
(C,f) is strict ConceptStr over (C)
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
the Intent of f is Element of bool the carrier' of C
bool the carrier' of C is non empty set
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
the Extent of f is Element of bool the carrier of C
bool the carrier of C is non empty set
a is Element of bool the carrier of (C)
b is Element of bool the carrier' of (C)
ConceptStr(# a,b #) is strict ConceptStr over (C)
bool the carrier of (C) is non empty Element of bool (bool the carrier of (C))
bool (bool the carrier of (C)) is non empty set
AttributeDerivation (C) is non empty V7() V10( bool the carrier' of (C)) V11( bool the carrier of (C)) Function-like V17( bool the carrier' of (C)) quasi_total Element of bool [:(bool the carrier' of (C)),(bool the carrier of (C)):]
bool the carrier' of (C) is non empty Element of bool (bool the carrier' of (C))
bool (bool the carrier' of (C)) is non empty set
[:(bool the carrier' of (C)),(bool the carrier of (C)):] is non empty set
bool [:(bool the carrier' of (C)),(bool the carrier of (C)):] is non empty set
the Intent of ConceptStr(# a,b #) is Element of bool the carrier' of (C)
(AttributeDerivation (C)) . the Intent of ConceptStr(# a,b #) is Element of bool the carrier of (C)
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
(ObjectDerivation C) . the Extent of f is Element of bool the carrier' of C
the Extent of ConceptStr(# a,b #) is Element of bool the carrier of (C)
ObjectDerivation (C) is non empty V7() V10( bool the carrier of (C)) V11( bool the carrier' of (C)) Function-like V17( bool the carrier of (C)) quasi_total Element of bool [:(bool the carrier of (C)),(bool the carrier' of (C)):]
[:(bool the carrier of (C)),(bool the carrier' of (C)):] is non empty set
bool [:(bool the carrier of (C)),(bool the carrier' of (C)):] is non empty set
(ObjectDerivation (C)) . the Extent of ConceptStr(# a,b #) is Element of bool the carrier' of (C)
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
(AttributeDerivation C) . the Intent of f is Element of bool the carrier of C
C is non quasi-empty strict ContextStr
(C) is non quasi-empty strict ContextStr
the carrier' of C is non empty set
the carrier of C is non empty set
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
f is strict non empty concept-like ConceptStr over C
(C,f) is strict non empty concept-like ConceptStr over (C)
((C),(C,f)) is strict non empty concept-like ConceptStr over ((C))
((C)) is non quasi-empty strict ContextStr
the carrier' of (C) is non empty set
the carrier of (C) is non empty set
the Information of (C) is V7() V10( the carrier of (C)) V11( the carrier' of (C)) Element of bool [: the carrier of (C), the carrier' of (C):]
[: the carrier of (C), the carrier' of (C):] is non empty set
bool [: the carrier of (C), the carrier' of (C):] is non empty set
the Information of (C) ~ is V7() V10( the carrier' of (C)) V11( the carrier of (C)) Element of bool [: the carrier' of (C), the carrier of (C):]
[: the carrier' of (C), the carrier of (C):] is non empty set
bool [: the carrier' of (C), the carrier of (C):] is non empty set
ContextStr(# the carrier' of (C), the carrier of (C),( the Information of (C) ~) #) is strict ContextStr
the Intent of ((C),(C,f)) is Element of bool the carrier' of ((C))
the carrier' of ((C)) is non empty set
bool the carrier' of ((C)) is non empty set
the Extent of (C,f) is Element of bool the carrier of (C)
bool the carrier of (C) is non empty set
the Intent of f is Element of bool the carrier' of C
bool the carrier' of C is non empty set
the Extent of ((C),(C,f)) is Element of bool the carrier of ((C))
the carrier of ((C)) is non empty set
bool the carrier of ((C)) is non empty set
the Intent of (C,f) is Element of bool the carrier' of (C)
bool the carrier' of (C) is non empty set
the Extent of f is Element of bool the carrier of C
bool the carrier of C is non empty set
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
(ConceptLattice C) .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of ((ConceptLattice C) .:) is non empty set
(C) is non quasi-empty strict ContextStr
the carrier' of C is non empty set
the carrier of C is non empty set
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
ConceptLattice (C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice (C)) is non empty set
bool the carrier of C is non empty set
bool the carrier' of C is non empty set
{ [ConceptStr(# b1,b2 #),(C,ConceptStr(# b1,b2 #))] where b1 is Element of bool the carrier of C, b2 is Element of bool the carrier' of C : ConceptStr(# b1,b2 #) is non empty concept-like ConceptStr over C } is set
B-carrier (C) is non empty Set-of-FormalConcepts of (C)
B-join (C) is non empty V7() V10([:(B-carrier (C)),(B-carrier (C)):]) V11( B-carrier (C)) Function-like V17([:(B-carrier (C)),(B-carrier (C)):]) quasi_total Element of bool [:[:(B-carrier (C)),(B-carrier (C)):],(B-carrier (C)):]
[:(B-carrier (C)),(B-carrier (C)):] is non empty set
[:[:(B-carrier (C)),(B-carrier (C)):],(B-carrier (C)):] is non empty set
bool [:[:(B-carrier (C)),(B-carrier (C)):],(B-carrier (C)):] is non empty set
B-meet (C) is non empty V7() V10([:(B-carrier (C)),(B-carrier (C)):]) V11( B-carrier (C)) Function-like V17([:(B-carrier (C)),(B-carrier (C)):]) quasi_total Element of bool [:[:(B-carrier (C)),(B-carrier (C)):],(B-carrier (C)):]
LattStr(# (B-carrier (C)),(B-join (C)),(B-meet (C)) #) is non empty strict LattStr
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
LattStr(# (B-carrier C),(B-meet C),(B-join C) #) is non empty strict LattStr
[: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C)):] is non empty set
a is set
b is Element of bool the carrier of C
a is Element of bool the carrier' of C
ConceptStr(# b,a #) is strict ConceptStr over C
(C,ConceptStr(# b,a #)) is strict ConceptStr over (C)
[ConceptStr(# b,a #),(C,ConceptStr(# b,a #))] is V1() set
{ConceptStr(# b,a #),(C,ConceptStr(# b,a #))} is set
{ConceptStr(# b,a #)} is set
{{ConceptStr(# b,a #),(C,ConceptStr(# b,a #))},{ConceptStr(# b,a #)}} is set
bool [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C)):] is non empty set
a is V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of (ConceptLattice (C))) Element of bool [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C)):]
dom a is Element of bool the carrier of ((ConceptLattice C) .:)
bool the carrier of ((ConceptLattice C) .:) is non empty set
b is set
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
(C,ConceptStr(# a,b #)) is strict ConceptStr over (C)
b is Element of the carrier of (ConceptLattice (C))
[b,b] is V1() set
{b,b} is set
{b} is set
{{b,b},{b}} is set
b is set
a is set
[b,a] is V1() set
{b,a} is set
{b} is set
{{b,a},{b}} is set
b is set
[b,b] is V1() set
{b,b} is set
{{b,b},{b}} is set
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
(C,ConceptStr(# a,b #)) is strict ConceptStr over (C)
[ConceptStr(# a,b #),(C,ConceptStr(# a,b #))] is V1() set
{ConceptStr(# a,b #),(C,ConceptStr(# a,b #))} is set
{ConceptStr(# a,b #)} is set
{{ConceptStr(# a,b #),(C,ConceptStr(# a,b #))},{ConceptStr(# a,b #)}} is set
Av is Element of bool the carrier of C
v is Element of bool the carrier' of C
ConceptStr(# Av,v #) is strict ConceptStr over C
(C,ConceptStr(# Av,v #)) is strict ConceptStr over (C)
[ConceptStr(# Av,v #),(C,ConceptStr(# Av,v #))] is V1() set
{ConceptStr(# Av,v #),(C,ConceptStr(# Av,v #))} is set
{ConceptStr(# Av,v #)} is set
{{ConceptStr(# Av,v #),(C,ConceptStr(# Av,v #))},{ConceptStr(# Av,v #)}} is set
[ConceptStr(# Av,v #),(C,ConceptStr(# Av,v #))] `1 is set
[b,a] `1 is set
[b,b] `1 is set
[ConceptStr(# a,b #),(C,ConceptStr(# a,b #))] `1 is set
[b,a] `2 is set
[b,b] `2 is set
the carrier of (ConceptLattice C) is non empty set
the L_meet of (ConceptLattice C) is non empty V7() V10([: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]) V11( the carrier of (ConceptLattice C)) Function-like V17([: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]) quasi_total Element of bool [:[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):], the carrier of (ConceptLattice C):]
[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):] is non empty set
[:[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):], the carrier of (ConceptLattice C):] is non empty set
bool [:[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):], the carrier of (ConceptLattice C):] is non empty set
the L_join of (ConceptLattice C) is non empty V7() V10([: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]) V11( the carrier of (ConceptLattice C)) Function-like V17([: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]) quasi_total Element of bool [:[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):], the carrier of (ConceptLattice C):]
LattStr(# the carrier of (ConceptLattice C), the L_meet of (ConceptLattice C), the L_join of (ConceptLattice C) #) is non empty strict LattStr
b is non empty V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of (ConceptLattice (C))) Function-like V17( the carrier of ((ConceptLattice C) .:)) quasi_total Element of bool [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C)):]
a is Element of the carrier of ((ConceptLattice C) .:)
b is Element of the carrier of ((ConceptLattice C) .:)
b . a is Element of the carrier of (ConceptLattice (C))
b . b is Element of the carrier of (ConceptLattice (C))
LattPOSet (ConceptLattice C) is non empty strict V82() V83() V84() RelStr
LattRel (ConceptLattice C) is V7() V10( the carrier of (ConceptLattice C)) V11( the carrier of (ConceptLattice C)) V17( the carrier of (ConceptLattice C)) quasi_total V89() V92() V96() Element of bool [: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]
bool [: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):] is non empty set
RelStr(# the carrier of (ConceptLattice C),(LattRel (ConceptLattice C)) #) is strict RelStr
the carrier of (LattPOSet (ConceptLattice C)) is non empty set
a % is Element of the carrier of (LattPOSet ((ConceptLattice C) .:))
LattPOSet ((ConceptLattice C) .:) is non empty strict V82() V83() V84() RelStr
LattRel ((ConceptLattice C) .:) is V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of ((ConceptLattice C) .:)) V17( the carrier of ((ConceptLattice C) .:)) quasi_total V89() V92() V96() Element of bool [: the carrier of ((ConceptLattice C) .:), the carrier of ((ConceptLattice C) .:):]
[: the carrier of ((ConceptLattice C) .:), the carrier of ((ConceptLattice C) .:):] is non empty set
bool [: the carrier of ((ConceptLattice C) .:), the carrier of ((ConceptLattice C) .:):] is non empty set
RelStr(# the carrier of ((ConceptLattice C) .:),(LattRel ((ConceptLattice C) .:)) #) is strict RelStr
the carrier of (LattPOSet ((ConceptLattice C) .:)) is non empty set
b % is Element of the carrier of (LattPOSet ((ConceptLattice C) .:))
dom b is Element of bool the carrier of ((ConceptLattice C) .:)
A is set
[a,A] is V1() set
{a,A} is set
{a} is set
{{a,A},{a}} is set
[(a %),(b %)] is V1() Element of [: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):]
[: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):] is non empty set
{(a %),(b %)} is set
{(a %)} is set
{{(a %),(b %)},{(a %)}} is set
the InternalRel of (LattPOSet ((ConceptLattice C) .:)) is V7() V10( the carrier of (LattPOSet ((ConceptLattice C) .:))) V11( the carrier of (LattPOSet ((ConceptLattice C) .:))) Element of bool [: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):]
bool [: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):] is non empty set
the InternalRel of (LattPOSet (ConceptLattice C)) is V7() V10( the carrier of (LattPOSet (ConceptLattice C))) V11( the carrier of (LattPOSet (ConceptLattice C))) Element of bool [: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):]
[: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):] is non empty set
bool [: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):] is non empty set
the InternalRel of (LattPOSet (ConceptLattice C)) ~ is V7() V10( the carrier of (LattPOSet (ConceptLattice C))) V11( the carrier of (LattPOSet (ConceptLattice C))) Element of bool [: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):]
[(b %),(a %)] is V1() Element of [: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):]
{(b %),(a %)} is set
{(b %)} is set
{{(b %),(a %)},{(b %)}} is set
b is Element of the carrier of (LattPOSet (ConceptLattice C))
a is Element of the carrier of (LattPOSet (ConceptLattice C))
% a is Element of the carrier of (ConceptLattice C)
(% a) % is Element of the carrier of (LattPOSet (ConceptLattice C))
% b is Element of the carrier of (ConceptLattice C)
(% b) % is Element of the carrier of (LattPOSet (ConceptLattice C))
(% b) @ is strict non empty concept-like ConceptStr over C
(% a) @ is strict non empty concept-like ConceptStr over C
fb is set
[b,fb] is V1() set
{b,fb} is set
{b} is set
{{b,fb},{b}} is set
rng b is Element of bool the carrier of (ConceptLattice (C))
bool the carrier of (ConceptLattice (C)) is non empty set
O9 is Element of bool the carrier of C
A9 is Element of bool the carrier' of C
ConceptStr(# O9,A9 #) is strict ConceptStr over C
(C,ConceptStr(# O9,A9 #)) is strict ConceptStr over (C)
[ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))] is V1() set
{ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))} is set
{ConceptStr(# O9,A9 #)} is set
{{ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))},{ConceptStr(# O9,A9 #)}} is set
[b,fb] `1 is set
[ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))] `1 is set
fb is Element of bool the carrier of C
fa is Element of bool the carrier' of C
ConceptStr(# fb,fa #) is strict ConceptStr over C
(C,ConceptStr(# fb,fa #)) is strict ConceptStr over (C)
[ConceptStr(# fb,fa #),(C,ConceptStr(# fb,fa #))] is V1() set
{ConceptStr(# fb,fa #),(C,ConceptStr(# fb,fa #))} is set
{ConceptStr(# fb,fa #)} is set
{{ConceptStr(# fb,fa #),(C,ConceptStr(# fb,fa #))},{ConceptStr(# fb,fa #)}} is set
fa is Element of the carrier of (ConceptLattice (C))
[a,fa] is V1() Element of [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C)):]
{a,fa} is set
{{a,fa},{a}} is set
[a,fa] `1 is Element of the carrier of ((ConceptLattice C) .:)
[ConceptStr(# fb,fa #),(C,ConceptStr(# fb,fa #))] `1 is set
fb is Element of the carrier of (ConceptLattice (C))
[b,fb] is V1() Element of [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C)):]
{b,fb} is set
{{b,fb},{b}} is set
[b,fb] `2 is Element of the carrier of (ConceptLattice (C))
[ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))] `2 is set
fb @ is strict non empty concept-like ConceptStr over (C)
the Intent of (fb @) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
the Intent of (C,ConceptStr(# O9,A9 #)) is Element of bool the carrier' of (C)
the Extent of ConceptStr(# O9,A9 #) is Element of bool the carrier of C
v is Element of the carrier of (ConceptLattice C)
v @ is strict non empty concept-like ConceptStr over C
the Extent of (v @) is Element of bool the carrier of C
[a,fa] `2 is Element of the carrier of (ConceptLattice (C))
[ConceptStr(# fb,fa #),(C,ConceptStr(# fb,fa #))] `2 is set
fa @ is strict non empty concept-like ConceptStr over (C)
the Intent of (fa @) is Element of bool the carrier' of (C)
the Intent of (C,ConceptStr(# fb,fa #)) is Element of bool the carrier' of (C)
the Extent of ConceptStr(# fb,fa #) is Element of bool the carrier of C
Av is Element of the carrier of (ConceptLattice C)
Av @ is strict non empty concept-like ConceptStr over C
the Extent of (Av @) is Element of bool the carrier of C
rng b is Element of bool the carrier of (ConceptLattice (C))
bool the carrier of (ConceptLattice (C)) is non empty set
a is set
dom b is Element of bool the carrier of ((ConceptLattice C) .:)
b is Element of the carrier of (ConceptLattice (C))
b @ is strict non empty concept-like ConceptStr over (C)
the Intent of (b @) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
the Extent of (b @) is Element of bool the carrier of (C)
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
the Intent of ConceptStr(# a,b #) is Element of bool the carrier' of C
(AttributeDerivation C) . the Intent of ConceptStr(# a,b #) is Element of bool the carrier of C
bool the carrier' of (C) is non empty Element of bool (bool the carrier' of (C))
bool (bool the carrier' of (C)) is non empty set
ObjectDerivation (C) is non empty V7() V10( bool the carrier of (C)) V11( bool the carrier' of (C)) Function-like V17( bool the carrier of (C)) quasi_total Element of bool [:(bool the carrier of (C)),(bool the carrier' of (C)):]
bool the carrier of (C) is non empty Element of bool (bool the carrier of (C))
bool (bool the carrier of (C)) is non empty set
[:(bool the carrier of (C)),(bool the carrier' of (C)):] is non empty set
bool [:(bool the carrier of (C)),(bool the carrier' of (C)):] is non empty set
(ObjectDerivation (C)) . the Extent of (b @) is Element of bool the carrier' of (C)
the Extent of ConceptStr(# a,b #) is Element of bool the carrier of C
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
(ObjectDerivation C) . the Extent of ConceptStr(# a,b #) is Element of bool the carrier' of C
AttributeDerivation (C) is non empty V7() V10( bool the carrier' of (C)) V11( bool the carrier of (C)) Function-like V17( bool the carrier' of (C)) quasi_total Element of bool [:(bool the carrier' of (C)),(bool the carrier of (C)):]
[:(bool the carrier' of (C)),(bool the carrier of (C)):] is non empty set
bool [:(bool the carrier' of (C)),(bool the carrier of (C)):] is non empty set
(AttributeDerivation (C)) . the Intent of (b @) is Element of bool the carrier of (C)
v is set
[ConceptStr(# a,b #),v] is V1() set
{ConceptStr(# a,b #),v} is set
{ConceptStr(# a,b #)} is set
{{ConceptStr(# a,b #),v},{ConceptStr(# a,b #)}} is set
A is Element of bool the carrier of C
fb is Element of bool the carrier' of C
ConceptStr(# A,fb #) is strict ConceptStr over C
(C,ConceptStr(# A,fb #)) is strict ConceptStr over (C)
[ConceptStr(# A,fb #),(C,ConceptStr(# A,fb #))] is V1() set
{ConceptStr(# A,fb #),(C,ConceptStr(# A,fb #))} is set
{ConceptStr(# A,fb #)} is set
{{ConceptStr(# A,fb #),(C,ConceptStr(# A,fb #))},{ConceptStr(# A,fb #)}} is set
[ConceptStr(# a,b #),v] `1 is set
[ConceptStr(# A,fb #),(C,ConceptStr(# A,fb #))] `1 is set
O9 is strict non empty concept-like ConceptStr over (C)
[ConceptStr(# a,b #),O9] is V1() set
{ConceptStr(# a,b #),O9} is set
{{ConceptStr(# a,b #),O9},{ConceptStr(# a,b #)}} is set
[ConceptStr(# a,b #),O9] `2 is set
[ConceptStr(# A,fb #),(C,ConceptStr(# A,fb #))] `2 is set
the Extent of O9 is Element of bool the carrier of (C)
the Intent of O9 is Element of bool the carrier' of (C)
a is set
proj1 b is set
b is set
b . a is set
b . b is set
dom b is Element of bool the carrier of ((ConceptLattice C) .:)
a is Element of the carrier of ((ConceptLattice C) .:)
Av is set
[a,Av] is V1() set
{a,Av} is set
{a} is set
{{a,Av},{a}} is set
b is Element of the carrier of ((ConceptLattice C) .:)
v is set
[b,v] is V1() set
{b,v} is set
{b} is set
{{b,v},{b}} is set
b . b is Element of the carrier of (ConceptLattice (C))
A is Element of bool the carrier of C
fb is Element of bool the carrier' of C
ConceptStr(# A,fb #) is strict ConceptStr over C
(C,ConceptStr(# A,fb #)) is strict ConceptStr over (C)
[ConceptStr(# A,fb #),(C,ConceptStr(# A,fb #))] is V1() set
{ConceptStr(# A,fb #),(C,ConceptStr(# A,fb #))} is set
{ConceptStr(# A,fb #)} is set
{{ConceptStr(# A,fb #),(C,ConceptStr(# A,fb #))},{ConceptStr(# A,fb #)}} is set
O9 is Element of bool the carrier of C
A9 is Element of bool the carrier' of C
ConceptStr(# O9,A9 #) is strict ConceptStr over C
(C,ConceptStr(# O9,A9 #)) is strict ConceptStr over (C)
[ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))] is V1() set
{ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))} is set
{ConceptStr(# O9,A9 #)} is set
{{ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))},{ConceptStr(# O9,A9 #)}} is set
the Intent of ConceptStr(# O9,A9 #) is Element of bool the carrier' of C
the Extent of (C,ConceptStr(# A,fb #)) is Element of bool the carrier of (C)
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
the Intent of ConceptStr(# A,fb #) is Element of bool the carrier' of C
the Extent of ConceptStr(# O9,A9 #) is Element of bool the carrier of C
the Intent of (C,ConceptStr(# A,fb #)) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
the Extent of ConceptStr(# A,fb #) is Element of bool the carrier of C
a is Element of the carrier of ((ConceptLattice C) .:)
b . a is Element of the carrier of (ConceptLattice (C))
b is Element of the carrier of ((ConceptLattice C) .:)
b . b is Element of the carrier of (ConceptLattice (C))
dom b is Element of bool the carrier of ((ConceptLattice C) .:)
a is set
[a,a] is V1() set
{a,a} is set
{a} is set
{{a,a},{a}} is set
(b . a) @ is strict non empty concept-like ConceptStr over (C)
(b . b) @ is strict non empty concept-like ConceptStr over (C)
v is Element of bool the carrier of C
A is Element of bool the carrier' of C
ConceptStr(# v,A #) is strict ConceptStr over C
(C,ConceptStr(# v,A #)) is strict ConceptStr over (C)
[ConceptStr(# v,A #),(C,ConceptStr(# v,A #))] is V1() set
{ConceptStr(# v,A #),(C,ConceptStr(# v,A #))} is set
{ConceptStr(# v,A #)} is set
{{ConceptStr(# v,A #),(C,ConceptStr(# v,A #))},{ConceptStr(# v,A #)}} is set
fb is set
[b,fb] is V1() set
{b,fb} is set
{b} is set
{{b,fb},{b}} is set
O9 is Element of bool the carrier of C
A9 is Element of bool the carrier' of C
ConceptStr(# O9,A9 #) is strict ConceptStr over C
(C,ConceptStr(# O9,A9 #)) is strict ConceptStr over (C)
[ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))] is V1() set
{ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))} is set
{ConceptStr(# O9,A9 #)} is set
{{ConceptStr(# O9,A9 #),(C,ConceptStr(# O9,A9 #))},{ConceptStr(# O9,A9 #)}} is set
fb is Element of the carrier of (ConceptLattice (C))
the Intent of ((b . b) @) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
fb @ is strict non empty concept-like ConceptStr over (C)
the Intent of (fb @) is Element of bool the carrier' of (C)
the Intent of (C,ConceptStr(# O9,A9 #)) is Element of bool the carrier' of (C)
the Extent of ConceptStr(# O9,A9 #) is Element of bool the carrier of C
Av is Element of the carrier of (ConceptLattice C)
Av @ is strict non empty concept-like ConceptStr over C
the Extent of (Av @) is Element of bool the carrier of C
fa is Element of the carrier of (ConceptLattice (C))
the Intent of ((b . a) @) is Element of bool the carrier' of (C)
fa @ is strict non empty concept-like ConceptStr over (C)
the Intent of (fa @) is Element of bool the carrier' of (C)
the Intent of (C,ConceptStr(# v,A #)) is Element of bool the carrier' of (C)
the Extent of ConceptStr(# v,A #) is Element of bool the carrier of C
b is Element of the carrier of (ConceptLattice C)
b @ is strict non empty concept-like ConceptStr over C
the Extent of (b @) is Element of bool the carrier of C
LattPOSet (ConceptLattice C) is non empty strict V82() V83() V84() RelStr
LattRel (ConceptLattice C) is V7() V10( the carrier of (ConceptLattice C)) V11( the carrier of (ConceptLattice C)) V17( the carrier of (ConceptLattice C)) quasi_total V89() V92() V96() Element of bool [: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]
bool [: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):] is non empty set
RelStr(# the carrier of (ConceptLattice C),(LattRel (ConceptLattice C)) #) is strict RelStr
Av % is Element of the carrier of (LattPOSet (ConceptLattice C))
the carrier of (LattPOSet (ConceptLattice C)) is non empty set
b % is Element of the carrier of (LattPOSet (ConceptLattice C))
[(Av %),(b %)] is V1() Element of [: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):]
[: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):] is non empty set
{(Av %),(b %)} is set
{(Av %)} is set
{{(Av %),(b %)},{(Av %)}} is set
the InternalRel of (LattPOSet (ConceptLattice C)) is V7() V10( the carrier of (LattPOSet (ConceptLattice C))) V11( the carrier of (LattPOSet (ConceptLattice C))) Element of bool [: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):]
bool [: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):] is non empty set
LattPOSet ((ConceptLattice C) .:) is non empty strict V82() V83() V84() RelStr
LattRel ((ConceptLattice C) .:) is V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of ((ConceptLattice C) .:)) V17( the carrier of ((ConceptLattice C) .:)) quasi_total V89() V92() V96() Element of bool [: the carrier of ((ConceptLattice C) .:), the carrier of ((ConceptLattice C) .:):]
[: the carrier of ((ConceptLattice C) .:), the carrier of ((ConceptLattice C) .:):] is non empty set
bool [: the carrier of ((ConceptLattice C) .:), the carrier of ((ConceptLattice C) .:):] is non empty set
RelStr(# the carrier of ((ConceptLattice C) .:),(LattRel ((ConceptLattice C) .:)) #) is strict RelStr
the carrier of (LattPOSet ((ConceptLattice C) .:)) is non empty set
a % is Element of the carrier of (LattPOSet ((ConceptLattice C) .:))
b % is Element of the carrier of (LattPOSet ((ConceptLattice C) .:))
[(a %),(b %)] is V1() Element of [: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):]
[: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):] is non empty set
{(a %),(b %)} is set
{(a %)} is set
{{(a %),(b %)},{(a %)}} is set
(LattPOSet (ConceptLattice C)) ~ is non empty strict V82() V83() V84() RelStr
the InternalRel of (LattPOSet (ConceptLattice C)) ~ is V7() V10( the carrier of (LattPOSet (ConceptLattice C))) V11( the carrier of (LattPOSet (ConceptLattice C))) Element of bool [: the carrier of (LattPOSet (ConceptLattice C)), the carrier of (LattPOSet (ConceptLattice C)):]
RelStr(# the carrier of (LattPOSet (ConceptLattice C)),( the InternalRel of (LattPOSet (ConceptLattice C)) ~) #) is strict RelStr
the InternalRel of ((LattPOSet (ConceptLattice C)) ~) is V7() V10( the carrier of ((LattPOSet (ConceptLattice C)) ~)) V11( the carrier of ((LattPOSet (ConceptLattice C)) ~)) Element of bool [: the carrier of ((LattPOSet (ConceptLattice C)) ~), the carrier of ((LattPOSet (ConceptLattice C)) ~):]
the carrier of ((LattPOSet (ConceptLattice C)) ~) is non empty set
[: the carrier of ((LattPOSet (ConceptLattice C)) ~), the carrier of ((LattPOSet (ConceptLattice C)) ~):] is non empty set
bool [: the carrier of ((LattPOSet (ConceptLattice C)) ~), the carrier of ((LattPOSet (ConceptLattice C)) ~):] is non empty set
the InternalRel of (LattPOSet ((ConceptLattice C) .:)) is V7() V10( the carrier of (LattPOSet ((ConceptLattice C) .:))) V11( the carrier of (LattPOSet ((ConceptLattice C) .:))) Element of bool [: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):]
bool [: the carrier of (LattPOSet ((ConceptLattice C) .:)), the carrier of (LattPOSet ((ConceptLattice C) .:)):] is non empty set
a is non empty V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of (ConceptLattice (C))) Function-like V17( the carrier of ((ConceptLattice C) .:)) quasi_total Homomorphism of (ConceptLattice C) .: , ConceptLattice (C)
b is strict non empty concept-like ConceptStr over C
a . b is set
(C,b) is strict non empty concept-like ConceptStr over (C)
dom a is Element of bool the carrier of ((ConceptLattice C) .:)
a is set
[b,a] is V1() set
{b,a} is set
{b} is set
{{b,a},{b}} is set
rng a is Element of bool the carrier of (ConceptLattice (C))
b is Element of bool the carrier of C
Av is Element of bool the carrier' of C
ConceptStr(# b,Av #) is strict ConceptStr over C
(C,ConceptStr(# b,Av #)) is strict ConceptStr over (C)
[ConceptStr(# b,Av #),(C,ConceptStr(# b,Av #))] is V1() set
{ConceptStr(# b,Av #),(C,ConceptStr(# b,Av #))} is set
{ConceptStr(# b,Av #)} is set
{{ConceptStr(# b,Av #),(C,ConceptStr(# b,Av #))},{ConceptStr(# b,Av #)}} is set
v is strict non empty concept-like ConceptStr over (C)
f is non empty V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of (ConceptLattice (C))) Function-like V17( the carrier of ((ConceptLattice C) .:)) quasi_total Homomorphism of (ConceptLattice C) .: , ConceptLattice (C)
a is non empty V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of (ConceptLattice (C))) Function-like V17( the carrier of ((ConceptLattice C) .:)) quasi_total Homomorphism of (ConceptLattice C) .: , ConceptLattice (C)
b is set
f . b is set
a . b is set
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
LattStr(# (B-carrier C),(B-meet C),(B-join C) #) is non empty strict LattStr
a is strict non empty concept-like ConceptStr over C
f . a is set
(C,a) is strict non empty concept-like ConceptStr over (C)
a . a is set
dom f is Element of bool the carrier of ((ConceptLattice C) .:)
bool the carrier of ((ConceptLattice C) .:) is non empty set
dom a is Element of bool the carrier of ((ConceptLattice C) .:)
C is non quasi-empty ContextStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
(ConceptLattice C) .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of ((ConceptLattice C) .:) is non empty set
(C) is non quasi-empty strict ContextStr
the carrier' of C is non empty set
the carrier of C is non empty set
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
ConceptLattice (C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (ConceptLattice (C)) is non empty set
(C) is non empty V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of (ConceptLattice (C))) Function-like V17( the carrier of ((ConceptLattice C) .:)) quasi_total Homomorphism of (ConceptLattice C) .: , ConceptLattice (C)
B-carrier C is non empty Set-of-FormalConcepts of C
B-join C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
[:(B-carrier C),(B-carrier C):] is non empty set
[:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):] is non empty set
B-meet C is non empty V7() V10([:(B-carrier C),(B-carrier C):]) V11( B-carrier C) Function-like V17([:(B-carrier C),(B-carrier C):]) quasi_total Element of bool [:[:(B-carrier C),(B-carrier C):],(B-carrier C):]
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
the carrier of (ConceptLattice C) is non empty set
the L_meet of (ConceptLattice C) is non empty V7() V10([: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]) V11( the carrier of (ConceptLattice C)) Function-like V17([: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]) quasi_total Element of bool [:[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):], the carrier of (ConceptLattice C):]
[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):] is non empty set
[:[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):], the carrier of (ConceptLattice C):] is non empty set
bool [:[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):], the carrier of (ConceptLattice C):] is non empty set
the L_join of (ConceptLattice C) is non empty V7() V10([: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]) V11( the carrier of (ConceptLattice C)) Function-like V17([: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):]) quasi_total Element of bool [:[: the carrier of (ConceptLattice C), the carrier of (ConceptLattice C):], the carrier of (ConceptLattice C):]
LattStr(# the carrier of (ConceptLattice C), the L_meet of (ConceptLattice C), the L_join of (ConceptLattice C) #) is non empty strict LattStr
rng (C) is Element of bool the carrier of (ConceptLattice (C))
bool the carrier of (ConceptLattice (C)) is non empty set
a is set
bool the carrier of C is non empty set
b is Element of the carrier of (ConceptLattice (C))
b @ is strict non empty concept-like ConceptStr over (C)
the Intent of (b @) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
bool the carrier' of C is non empty set
the Extent of (b @) is Element of bool the carrier of (C)
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
a is Element of bool the carrier of C
b is Element of bool the carrier' of C
ConceptStr(# a,b #) is strict ConceptStr over C
bool the carrier of C is non empty Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
AttributeDerivation C is non empty V7() V10( bool the carrier' of C) V11( bool the carrier of C) Function-like V17( bool the carrier' of C) quasi_total Element of bool [:(bool the carrier' of C),(bool the carrier of C):]
bool the carrier' of C is non empty Element of bool (bool the carrier' of C)
bool (bool the carrier' of C) is non empty set
[:(bool the carrier' of C),(bool the carrier of C):] is non empty set
bool [:(bool the carrier' of C),(bool the carrier of C):] is non empty set
the Intent of ConceptStr(# a,b #) is Element of bool the carrier' of C
(AttributeDerivation C) . the Intent of ConceptStr(# a,b #) is Element of bool the carrier of C
bool the carrier' of (C) is non empty Element of bool (bool the carrier' of (C))
bool (bool the carrier' of (C)) is non empty set
ObjectDerivation (C) is non empty V7() V10( bool the carrier of (C)) V11( bool the carrier' of (C)) Function-like V17( bool the carrier of (C)) quasi_total Element of bool [:(bool the carrier of (C)),(bool the carrier' of (C)):]
bool the carrier of (C) is non empty Element of bool (bool the carrier of (C))
bool (bool the carrier of (C)) is non empty set
[:(bool the carrier of (C)),(bool the carrier' of (C)):] is non empty set
bool [:(bool the carrier of (C)),(bool the carrier' of (C)):] is non empty set
(ObjectDerivation (C)) . the Extent of (b @) is Element of bool the carrier' of (C)
the Extent of ConceptStr(# a,b #) is Element of bool the carrier of C
ObjectDerivation C is non empty V7() V10( bool the carrier of C) V11( bool the carrier' of C) Function-like V17( bool the carrier of C) quasi_total Element of bool [:(bool the carrier of C),(bool the carrier' of C):]
[:(bool the carrier of C),(bool the carrier' of C):] is non empty set
bool [:(bool the carrier of C),(bool the carrier' of C):] is non empty set
(ObjectDerivation C) . the Extent of ConceptStr(# a,b #) is Element of bool the carrier' of C
AttributeDerivation (C) is non empty V7() V10( bool the carrier' of (C)) V11( bool the carrier of (C)) Function-like V17( bool the carrier' of (C)) quasi_total Element of bool [:(bool the carrier' of (C)),(bool the carrier of (C)):]
[:(bool the carrier' of (C)),(bool the carrier of (C)):] is non empty set
bool [:(bool the carrier' of (C)),(bool the carrier of (C)):] is non empty set
(AttributeDerivation (C)) . the Intent of (b @) is Element of bool the carrier of (C)
b is strict non empty concept-like ConceptStr over C
(C,b) is strict non empty concept-like ConceptStr over (C)
the Extent of (C,b) is Element of bool the carrier of (C)
(C) . b is set
the Intent of (C,b) is Element of bool the carrier' of (C)
dom (C) is Element of bool the carrier of ((ConceptLattice C) .:)
bool the carrier of ((ConceptLattice C) .:) is non empty set
a is set
proj1 (C) is set
b is set
(C) . a is set
(C) . b is set
dom (C) is Element of bool the carrier of ((ConceptLattice C) .:)
bool the carrier of ((ConceptLattice C) .:) is non empty set
a is Element of the carrier of ((ConceptLattice C) .:)
b is Element of the carrier of ((ConceptLattice C) .:)
a is Element of the carrier of (ConceptLattice C)
a @ is strict non empty concept-like ConceptStr over C
(C) . (a @) is set
(C) . a is set
b is Element of the carrier of (ConceptLattice C)
b @ is strict non empty concept-like ConceptStr over C
(C) . (b @) is set
(C) . b is set
(C,(a @)) is strict non empty concept-like ConceptStr over (C)
(C,(b @)) is strict non empty concept-like ConceptStr over (C)
the Extent of (a @) is Element of bool the carrier of C
bool the carrier of C is non empty set
the Intent of (C,(b @)) is Element of bool the carrier' of (C)
the carrier' of (C) is non empty set
bool the carrier' of (C) is non empty set
the Extent of (b @) is Element of bool the carrier of C
the Intent of (a @) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
the Extent of (C,(b @)) is Element of bool the carrier of (C)
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
the Intent of (b @) is Element of bool the carrier' of C
C is non quasi-empty ContextStr
(C) is non quasi-empty strict ContextStr
the carrier' of C is non empty set
the carrier of C is non empty set
the Information of C is V7() V10( the carrier of C) V11( the carrier' of C) Element of bool [: the carrier of C, the carrier' of C:]
[: the carrier of C, the carrier' of C:] is non empty set
bool [: the carrier of C, the carrier' of C:] is non empty set
the Information of C ~ is V7() V10( the carrier' of C) V11( the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]
[: the carrier' of C, the carrier of C:] is non empty set
bool [: the carrier' of C, the carrier of C:] is non empty set
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is strict ContextStr
ConceptLattice (C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
ConceptLattice C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
(ConceptLattice C) .: is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
the carrier of ((ConceptLattice C) .:) is non empty set
the carrier of (ConceptLattice (C)) is non empty set
(C) is non empty V7() V10( the carrier of ((ConceptLattice C) .:)) V11( the carrier of (ConceptLattice (C))) Function-like V17( the carrier of ((ConceptLattice C) .:)) quasi_total Homomorphism of (ConceptLattice C) .: , ConceptLattice (C)