:: CONLAT_2 semantic presentation

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) . b

meet { ((ObjectDerivation C) . b

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

{ b

( not b

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

{ b

( not b

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) . b

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

{ b

( not b

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

{ b

( not b

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) . b

meet { ((AttributeDerivation C) . b

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

{ b

( not b

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

{ b

( not b

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) . b

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

{ b

( not b

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

{ b

( not b

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)

{ b

"\/" ( { b

"\/" (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)

{ b

"\/" ( { b

"\/" (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)

{ b

"\/" ( { b

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)

{ b

"\/" ( { b

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(# b

union { the Extent of ConceptStr(# b

(ObjectDerivation C) . (union { the Extent of ConceptStr(# b

(AttributeDerivation C) . ((ObjectDerivation C) . (union { the Extent of ConceptStr(# b

the Intent of (C,f) is Element of bool the carrier' of C

{ the Intent of ConceptStr(# b

meet { the Intent of ConceptStr(# b

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) . b

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) . b

meet { ((ObjectDerivation C) . b

the Element of { the Intent of ConceptStr(# b

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)

{ b

"\/" ( { b

the Extent of (C,f) is Element of bool the carrier of C

{ the Extent of ConceptStr(# b

meet { the Extent of ConceptStr(# b

the Intent of (C,f) is Element of bool the carrier' of C

{ the Intent of ConceptStr(# b

union { the Intent of ConceptStr(# b

(AttributeDerivation C) . (union { the Intent of ConceptStr(# b

(ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# b

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) . b

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) . b

meet { ((AttributeDerivation C) . b

the Element of { the Extent of ConceptStr(# b

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(# b

( b

"\/" ( { ConceptStr(# b

( b

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(# b

( b

"/\" ( { ConceptStr(# b

( b

the carrier of (ConceptLattice C) is non empty set

{ b

( b

"\/" ( { b

( b

(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(# 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

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(# b

( b

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(# b

( b

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(# b

( b

{ b

( b

"\/" ( { b

( b

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

{ b

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

{ b

"\/" ( { b

b is Element of the carrier of f

"/\" ({(a . b),(a . a)},f) is Element of the carrier of f

{ b

"\/" ( { b

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 . b

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 . b

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)

{ b

"\/" ( { b

{ (a . b

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 <