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 <