let L be complete Lattice; :: thesis:
let C be FormalContext; :: thesis:

hereby :: thesis:

assume ConceptLattice C,L are_isomorphic ; :: thesis:
then consider f being Homomorphism of ConceptLattice C,L such that
A1: f is bijective by LATTICE4:def 5;
A2: ( f is one-to-one & f is onto ) by A1;
take g = f * (gamma C); :: thesis:
take d = f * (delta C); :: thesis:
thus rng g is supremum-dense :: thesis:

proof

let a be Element of L; :: according to LATTICE6:def 13 :: thesis:
consider b being Element of (ConceptLattice C) such that
A3: a = f . b by A2, LATTICE4:9;
rng (gamma C) is supremum-dense by Th12;
then consider D' being Subset of (rng (gamma C)) such that
A4: b = "\/" D',(ConceptLattice C) by LATTICE6:def 13;
A5: ( D' is_less_than b & ( for r being Element of (ConceptLattice C) st D' is_less_than r holds
b [= r ) ) by A4, LATTICE3:def 21;
set D = { (f . x) where x is Element of (ConceptLattice C) : x in D' } ;
A6: { (f . x) where x is Element of (ConceptLattice C) : x in D' } c= rng g

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (f . x) where x is Element of (ConceptLattice C) : x in D' } ; :: thesis:
then consider x' being Element of (ConceptLattice C) such that
A7: ( x = f . x' & x' in D' ) ;
consider y being set such that
A8: ( y in dom (gamma C) & (gamma C) . y = x' ) by A7, FUNCT_1:def 5;
A9: x = (f * (gamma C)) . y by A7, A8, FUNCT_1:23;
dom f = the carrier of (ConceptLattice C) by FUNCT_2:def 1;
then y in dom (f * (gamma C)) by A8, FUNCT_1:21;
hence x in rng g by A9, FUNCT_1:def 5; :: thesis:

end;

A10: { (f . x) where x is Element of (ConceptLattice C) : x in D' } is_less_than a

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis:
assume q in { (f . x) where x is Element of (ConceptLattice C) : x in D' } ; :: thesis:
then consider q' being Element of (ConceptLattice C) such that
A11: ( q = f . q' & q' in D' ) ;
q' [= b by A5, A11, LATTICE3:def 17;
hence q [= a by A2, A3, A11, LATTICE4:8; :: thesis:

end;

for r being Element of L st { (f . x) where x is Element of (ConceptLattice C) : x in D' } is_less_than r holds
a [= r

proof

let r be Element of L; :: thesis:
assume A12: { (f . x) where x is Element of (ConceptLattice C) : x in D' } is_less_than r ; :: thesis:
consider r' being Element of (ConceptLattice C) such that
A13: r = f . r' by A2, LATTICE4:9;
reconsider r' = r' as Element of (ConceptLattice C) ;
for q being Element of (ConceptLattice C) st q in D' holds
q [= r'

proof

let q be Element of (ConceptLattice C); :: thesis:
assume q in D' ; :: thesis:
then f . q in { (f . x) where x is Element of (ConceptLattice C) : x in D' } ;
then f . q [= f . r' by A12, A13, LATTICE3:def 17;
hence q [= r' by A2, LATTICE4:8; :: thesis:

end;

then D' is_less_than r' by LATTICE3:def 17;
then b [= r' by A4, LATTICE3:def 21;
hence a [= r by A2, A3, A13, LATTICE4:8; :: thesis:

end;

then a = "\/" { (f . x) where x is Element of (ConceptLattice C) : x in D' } ,L by A10, LATTICE3:def 21;
hence ex b₁ being Element of bool (rng g) st a = "\/" b₁,L by A6; :: thesis:

end;

thus rng d is infimum-dense :: thesis:

proof

let a be Element of L; :: according to LATTICE6:def 14 :: thesis:
consider b being Element of (ConceptLattice C) such that
A14: a = f . b by A2, LATTICE4:9;
rng (delta C) is infimum-dense by Th12;
then consider D' being Subset of (rng (delta C)) such that
A15: b = "/\" D',(ConceptLattice C) by LATTICE6:def 14;
A16: ( b is_less_than D' & ( for r being Element of (ConceptLattice C) st r is_less_than D' holds
r [= b ) ) by A15, LATTICE3:34;
set D = { (f . x) where x is Element of (ConceptLattice C) : x in D' } ;
A17: { (f . x) where x is Element of (ConceptLattice C) : x in D' } c= rng d

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (f . x) where x is Element of (ConceptLattice C) : x in D' } ; :: thesis:
then consider x' being Element of (ConceptLattice C) such that
A18: ( x = f . x' & x' in D' ) ;
consider y being set such that
A19: ( y in dom (delta C) & (delta C) . y = x' ) by A18, FUNCT_1:def 5;
A20: x = (f * (delta C)) . y by A18, A19, FUNCT_1:23;
dom f = the carrier of (ConceptLattice C) by FUNCT_2:def 1;
then y in dom (f * (delta C)) by A19, FUNCT_1:21;
hence x in rng d by A20, FUNCT_1:def 5; :: thesis:

end;

A21: a is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D' }

proof

let q be Element of L; :: according to LATTICE3:def 16 :: thesis:
assume q in { (f . x) where x is Element of (ConceptLattice C) : x in D' } ; :: thesis:
then consider q' being Element of (ConceptLattice C) such that
A22: ( q = f . q' & q' in D' ) ;
b [= q' by A16, A22, LATTICE3:def 16;
hence a [= q by A2, A14, A22, LATTICE4:8; :: thesis:

end;

for r being Element of L st r is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D' } holds
r [= a

proof

let r be Element of L; :: thesis:
assume A23: r is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D' } ; :: thesis:
consider r' being Element of (ConceptLattice C) such that
A24: r = f . r' by A2, LATTICE4:9;
reconsider r' = r' as Element of (ConceptLattice C) ;
r' is_less_than D'

proof

let q be Element of (ConceptLattice C); :: according to LATTICE3:def 16 :: thesis:
assume q in D' ; :: thesis:
then f . q in { (f . x) where x is Element of (ConceptLattice C) : x in D' } ;
then f . r' [= f . q by A23, A24, LATTICE3:def 16;
hence r' [= q by A2, LATTICE4:8; :: thesis:

end;

then r' [= b by A15, LATTICE3:34;
hence r [= a by A2, A14, A24, LATTICE4:8; :: thesis:

end;

then a = "/\" { (f . x) where x is Element of (ConceptLattice C) : x in D' } ,L by A21, LATTICE3:34;
hence ex b₁ being Element of bool (rng d) st a = "/\" b₁,L by A17; :: thesis:

end;

let o be Object of C; :: thesis:
let a be Attribute of C; :: thesis:
A25: ( o is-connected-with a iff (gamma C) . o [= (delta C) . a ) by Th13;

hereby :: thesis:

assume A26: o is-connected-with a ; :: thesis:
( dom (gamma C) = the carrier of C & dom (delta C) = the carrier' of C ) by FUNCT_2:def 1;
then ( f . ((gamma C) . o) = (f * (gamma C)) . o & f . ((delta C) . a) = (f * (delta C)) . a ) by FUNCT_1:23;
hence g . o [= d . a by A2, A25, A26, LATTICE4:8; :: thesis:

end;

assume A27: g . o [= d . a ; :: thesis:
( dom (gamma C) = the carrier of C & dom (delta C) = the carrier' of C ) by FUNCT_2:def 1;
then ( f . ((gamma C) . o) = (f * (gamma C)) . o & f . ((delta C) . a) = (f * (delta C)) . a ) by FUNCT_1:23;
then (gamma C) . o [= (delta C) . a by A2, A27, LATTICE4:8;
hence o is-connected-with a by Th13; :: thesis:

end;

given g being Function of the carrier of C,the carrier of L, d being Function of the carrier' of C,the carrier of L such that A28: ( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of C
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ) ) ; :: thesis:
set f = { [ConceptStr(# O,A #),x] where O is Subset of the carrier of C, A is Subset of the carrier' of C, x is Element of L : ( ConceptStr(# O,A #) is FormalConcept of C & x = "\/" { (g . o) where o is Object of C : o in O } ,L ) } ;
A29: ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 23;
{ [ConceptStr(# O,A #),x] where O is Subset of the carrier of C, A is Subset of the carrier' of C, x is Element of L : ( ConceptStr(# O,A #) is FormalConcept of C & x = "\/" { (g . o) where o is Object of C : o in O } ,L ) } c= [:the carrier of (ConceptLattice C),the carrier of L:]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in { [ConceptStr(# O,A #),x] where O is Subset of the carrier of C, A is Subset of the carrier' of C, x is Element of L : ( ConceptStr(# O,A #) is FormalConcept of C & x = "\/" { (g . o) where o is Object of C : o in O } ,L ) } ; :: thesis:
then consider O being Subset of the carrier of C, A being Subset of the carrier' of C, x being Element of L such that
A30: ( y = [ConceptStr(# O,A #),x] & ConceptStr(# O,A #) is FormalConcept of C & x = "\/" { (g . o) where o is Object of C : o in O } ,L ) ;
ConceptStr(# O,A #) in the carrier of (ConceptLattice C) by A29, A30, CONLAT_1:35;
hence y in [:the carrier of (ConceptLattice C),the carrier of L:] by A30, ZFMISC_1:def 2; :: thesis:

end;

then reconsider f = { [ConceptStr(# O,A #),x] where O is Subset of the carrier of C, A is Subset of the carrier' of C, x is Element of L : ( ConceptStr(# O,A #) is FormalConcept of C & x = "\/" { (g . o) where o is Object of C : o in O } ,L ) } as Relation of the carrier of (ConceptLattice C),the carrier of L ;
the carrier of (ConceptLattice C) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in the carrier of (ConceptLattice C) ; :: thesis:
then A31: y is strict FormalConcept of C by A29, CONLAT_1:35;
then consider O' being Subset of the carrier of C, A' being Subset of the carrier' of C such that
A32: y = ConceptStr(# O',A' #) ;
reconsider z = "\/" { (g . o) where o is Object of C : o in O' } ,L as Element of L ;
[y,z] in f by A31, A32;
hence y in dom f by RELAT_1:def 4; :: thesis:

end;

then A33: the carrier of (ConceptLattice C) = dom f by XBOOLE_0:def 10;
for x, y1, y2 being set st [x,y1] in f & [x,y2] in f holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis:
assume A34: ( [x,y1] in f & [x,y2] in f ) ; :: thesis:
then consider O being Subset of the carrier of C, A being Subset of the carrier' of C, z being Element of L such that
A35: ( [x,y1] = [ConceptStr(# O,A #),z] & ConceptStr(# O,A #) is FormalConcept of C & z = "\/" { (g . o) where o is Object of C : o in O } ,L ) ;
consider O' being Subset of the carrier of C, A' being Subset of the carrier' of C, z' being Element of L such that
A36: ( [x,y2] = [ConceptStr(# O',A' #),z'] & ConceptStr(# O',A' #) is FormalConcept of C & z' = "\/" { (g . o) where o is Object of C : o in O' } ,L ) by A34;
ConceptStr(# O,A #) = [x,y1] `1 by A35, MCART_1:def 1
.= x by MCART_1:def 1
.= [x,y2] `1 by MCART_1:def 1
.= ConceptStr(# O',A' #) by A36, MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A35, A36, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis:

end;

then reconsider f = f as Function of the carrier of (ConceptLattice C),the carrier of L by A33, FUNCT_1:def 1, FUNCT_2:def 1;
A37: ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 23;
A38: for a, b being Element of (ConceptLattice C) st a [= b holds
f . a [= f . b

proof

let a, b be Element of (ConceptLattice C); :: thesis:
assume a [= b ; :: thesis:
then a @ is-SubConcept-of b @ by CONLAT_1:47;
then A39: the Extent of (a @ ) c= the Extent of (b @ ) by CONLAT_1:def 19;
A40: { (g . o) where o is Object of C : o in the Extent of (a @ ) } c= { (g . o) where o is Object of C : o in the Extent of (b @ ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (g . o) where o is Object of C : o in the Extent of (a @ ) } ; :: thesis:
then consider o being Object of C such that
A41: ( x = g . o & o in the Extent of (a @ ) ) ;
thus x in { (g . o) where o is Object of C : o in the Extent of (b @ ) } by A39, A41; :: thesis:

end;

reconsider xa = "\/" { (g . o) where o is Object of C : o in the Extent of (a @ ) } ,L, xb = "\/" { (g . o) where o is Object of C : o in the Extent of (b @ ) } ,L as Element of L ;
( [(a @ ),xa] in f & [(b @ ),xb] in f ) ;
then A42: ( f . (a @ ) = xa & f . (b @ ) = xb ) by FUNCT_1:8;
( a @ = a & b @ = b ) by CONLAT_1:def 24;
hence f . a [= f . b by A40, A42, LATTICE3:46; :: thesis:

end;

set fi = { [x,ConceptStr(# O,A #)] where x is Element of L, O is Subset of the carrier of C, A is Subset of the carrier' of C : ( O = { o where o is Object of C : g . o [= x } & A = { a where a is Attribute of C : x [= d . a } ) } ;
{ [x,ConceptStr(# O,A #)] where x is Element of L, O is Subset of the carrier of C, A is Subset of the carrier' of C : ( O = { o where o is Object of C : g . o [= x } & A = { a where a is Attribute of C : x [= d . a } ) } c= [:the carrier of L,the carrier of (ConceptLattice C):]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in { [x,ConceptStr(# O,A #)] where x is Element of L, O is Subset of the carrier of C, A is Subset of the carrier' of C : ( O = { o where o is Object of C : g . o [= x } & A = { a where a is Attribute of C : x [= d . a } ) } ; :: thesis:
then consider x being Element of L, O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A43: ( y = [x,ConceptStr(# O,A #)] & O = { o where o is Object of C : g . o [= x } & A = { a where a is Attribute of C : x [= d . a } ) ;
A44: (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) = the Intent of ConceptStr(# O,A #)

proof

thus (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) c= the Intent of ConceptStr(# O,A #) :: according to XBOOLE_0:def 10 :: thesis:

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) ; :: thesis:
then u in { o where o is Attribute of C : for a being Object of C st a in the Extent of ConceptStr(# O,A #) holds
a is-connected-with o } by CONLAT_1:def 6;
then consider u' being Attribute of C such that
A45: ( u' = u & ( for a being Object of C st a in the Extent of ConceptStr(# O,A #) holds
a is-connected-with u' ) ) ;
A46: for v being Object of C st v in { a where a is Object of C : g . a [= x } holds
g . v [= d . u'

proof

let v be Object of C; :: thesis:
assume v in { a where a is Object of C : g . a [= x } ; :: thesis:
then v is-connected-with u' by A43, A45;
hence g . v [= d . u' by A28; :: thesis:

end;

A47: { (g . a) where a is Object of C : g . a [= x } is_less_than d . u'

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis:
assume q in { (g . a) where a is Object of C : g . a [= x } ; :: thesis:
then consider b being Object of C such that
A48: ( q = g . b & g . b [= x ) ;
b in { a where a is Object of C : g . a [= x } by A48;
hence q [= d . u' by A46, A48; :: thesis:

end;

"\/" { (g . a') where a' is Object of C : g . a' [= x } ,L = x

proof

consider D being Subset of (rng g) such that
A49: "\/" D,L = x by A28, LATTICE6:def 13;
A50: D is_less_than x by A49, LATTICE3:def 21;
D c= { (g . a') where a' is Object of C : g . a' [= x }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A51: u in D ; :: thesis:
then consider v being set such that
A52: ( v in dom g & u = g . v ) by FUNCT_1:def 5;
reconsider v = v as Object of C by A52;
g . v [= x by A50, A51, A52, LATTICE3:def 17;
hence u in { (g . a') where a' is Object of C : g . a' [= x } by A52; :: thesis:

end;

then A53: x [= "\/" { (g . a') where a' is Object of C : g . a' [= x } ,L by A49, LATTICE3:46;
{ (g . a') where a' is Object of C : g . a' [= x } is_less_than x

proof

let u be Element of L; :: according to LATTICE3:def 17 :: thesis:
assume u in { (g . a') where a' is Object of C : g . a' [= x } ; :: thesis:
then consider v being Object of C such that
A54: ( u = g . v & g . v [= x ) ;
thus u [= x by A54; :: thesis:

end;

then "\/" { (g . a') where a' is Object of C : g . a' [= x } ,L [= x by LATTICE3:def 21;
hence "\/" { (g . a') where a' is Object of C : g . a' [= x } ,L = x by A53, LATTICES:26; :: thesis:

end;

then x [= d . u' by A47, LATTICE3:def 21;
hence u in the Intent of ConceptStr(# O,A #) by A43, A45; :: thesis:

end;

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in the Intent of ConceptStr(# O,A #) ; :: thesis:
then consider u' being Attribute of C such that
A55: ( u' = u & x [= d . u' ) by A43;
A56: for v being Object of C st v in { a where a is Object of C : g . a [= x } holds
g . v [= d . u'

proof

let v be Object of C; :: thesis:
assume v in { a where a is Object of C : g . a [= x } ; :: thesis:
then consider v' being Object of C such that
A57: ( v' = v & g . v' [= x ) ;
thus g . v [= d . u' by A55, A57, LATTICES:25; :: thesis:

end;

for v being Object of C st v in { a where a is Object of C : g . a [= x } holds
v is-connected-with u'

proof

let v be Object of C; :: thesis:
assume v in { a where a is Object of C : g . a [= x } ; :: thesis:
then g . v [= d . u' by A56;
hence v is-connected-with u' by A28; :: thesis:

end;

then u' in { o where o is Attribute of C : for a being Object of C st a in the Extent of ConceptStr(# O,A #) holds
a is-connected-with o } by A43;
hence u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) by A55, CONLAT_1:def 6; :: thesis:

end;

(AttributeDerivation C) . the Intent of ConceptStr(# O,A #) = the Extent of ConceptStr(# O,A #)

proof

thus (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) c= the Extent of ConceptStr(# O,A #) :: according to XBOOLE_0:def 10 :: thesis:

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) ; :: thesis:
then u in { o where o is Object of C : for a being Attribute of C st a in the Intent of ConceptStr(# O,A #) holds
o is-connected-with a } by CONLAT_1:def 7;
then consider u' being Object of C such that
A58: ( u' = u & ( for a being Attribute of C st a in the Intent of ConceptStr(# O,A #) holds
u' is-connected-with a ) ) ;
A59: for v being Attribute of C st v in { a where a is Attribute of C : x [= d . a } holds
g . u' [= d . v

proof

let v be Attribute of C; :: thesis:
assume v in { a where a is Attribute of C : x [= d . a } ; :: thesis:
then u' is-connected-with v by A43, A58;
hence g . u' [= d . v by A28; :: thesis:

end;

A60: g . u' is_less_than { (d . a) where a is Attribute of C : x [= d . a }

proof

let q be Element of L; :: according to LATTICE3:def 16 :: thesis:
assume q in { (d . a) where a is Attribute of C : x [= d . a } ; :: thesis:
then consider b being Attribute of C such that
A61: ( q = d . b & x [= d . b ) ;
b in { a where a is Attribute of C : x [= d . a } by A61;
hence g . u' [= q by A59, A61; :: thesis:

end;

"/\" { (d . a') where a' is Attribute of C : x [= d . a' } ,L = x

proof

consider D being Subset of (rng d) such that
A62: "/\" D,L = x by A28, LATTICE6:def 14;
A63: x is_less_than D by A62, LATTICE3:34;
D c= { (d . a') where a' is Attribute of C : x [= d . a' }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A64: u in D ; :: thesis:
then consider v being set such that
A65: ( v in dom d & u = d . v ) by FUNCT_1:def 5;
reconsider v = v as Attribute of C by A65;
x [= d . v by A63, A64, A65, LATTICE3:def 16;
hence u in { (d . a') where a' is Attribute of C : x [= d . a' } by A65; :: thesis:

end;

then A66: "/\" { (d . a') where a' is Attribute of C : x [= d . a' } ,L [= x by A62, LATTICE3:46;
x is_less_than { (d . a') where a' is Attribute of C : x [= d . a' }

proof

let u be Element of L; :: according to LATTICE3:def 16 :: thesis:
assume u in { (d . a') where a' is Attribute of C : x [= d . a' } ; :: thesis:
then consider v being Attribute of C such that
A67: ( u = d . v & x [= d . v ) ;
thus x [= u by A67; :: thesis:

end;

then x [= "/\" { (d . a') where a' is Attribute of C : x [= d . a' } ,L by LATTICE3:40;
hence "/\" { (d . a') where a' is Attribute of C : x [= d . a' } ,L = x by A66, LATTICES:26; :: thesis:

end;

then g . u' [= x by A60, LATTICE3:34;
hence u in the Extent of ConceptStr(# O,A #) by A43, A58; :: thesis:

end;

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in the Extent of ConceptStr(# O,A #) ; :: thesis:
then consider u' being Object of C such that
A68: ( u' = u & g . u' [= x ) by A43;
A69: for v being Attribute of C st v in { a where a is Attribute of C : x [= d . a } holds
g . u' [= d . v

proof

let v be Attribute of C; :: thesis:
assume v in { a where a is Attribute of C : x [= d . a } ; :: thesis:
then consider v' being Attribute of C such that
A70: ( v' = v & x [= d . v' ) ;
thus g . u' [= d . v by A68, A70, LATTICES:25; :: thesis:

end;

for v being Attribute of C st v in { a where a is Attribute of C : x [= d . a } holds
u' is-connected-with v

proof

let v be Attribute of C; :: thesis:
assume v in { a where a is Attribute of C : x [= d . a } ; :: thesis:
then g . u' [= d . v by A69;
hence u' is-connected-with v by A28; :: thesis:

end;

then u' in { o where o is Object of C : for a being Attribute of C st a in the Intent of ConceptStr(# O,A #) holds
o is-connected-with a } by A43;
hence u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) by A68, CONLAT_1:def 7; :: thesis:

end;

then ConceptStr(# O,A #) is FormalConcept of C by A44, Lm3, CONLAT_1:def 13;
then ConceptStr(# O,A #) in the carrier of (ConceptLattice C) by A29, CONLAT_1:35;
hence y in [:the carrier of L,the carrier of (ConceptLattice C):] by A43, ZFMISC_1:def 2; :: thesis:

end;

then reconsider fi = { [x,ConceptStr(# O,A #)] where x is Element of L, O is Subset of the carrier of C, A is Subset of the carrier' of C : ( O = { o where o is Object of C : g . o [= x } & A = { a where a is Attribute of C : x [= d . a } ) } as Relation of the carrier of L,the carrier of (ConceptLattice C) ;
the carrier of L c= dom fi

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in the carrier of L ; :: thesis:
then reconsider y = y as Element of L ;
set O = { o where o is Object of C : g . o [= y } ;
set A = { a where a is Attribute of C : y [= d . a } ;
{ o where o is Object of C : g . o [= y } c= the carrier of C

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { o where o is Object of C : g . o [= y } ; :: thesis:
then consider u' being Object of C such that
A71: ( u' = u & g . u' [= y ) ;
thus u in the carrier of C by A71; :: thesis:

end;

then reconsider O = { o where o is Object of C : g . o [= y } as Subset of the carrier of C ;
{ a where a is Attribute of C : y [= d . a } c= the carrier' of C

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { a where a is Attribute of C : y [= d . a } ; :: thesis:
then consider u' being Attribute of C such that
A72: ( u' = u & y [= d . u' ) ;
thus u in the carrier' of C by A72; :: thesis:

end;

then reconsider A = { a where a is Attribute of C : y [= d . a } as Subset of the carrier' of C ;
[y,ConceptStr(# O,A #)] in fi ;
hence y in dom fi by RELAT_1:def 4; :: thesis:

end;

then A73: the carrier of L = dom fi by XBOOLE_0:def 10;
for x, y1, y2 being set st [x,y1] in fi & [x,y2] in fi holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis:
assume A74: ( [x,y1] in fi & [x,y2] in fi ) ; :: thesis:
then consider z being Element of L, O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A75: ( [x,y1] = [z,ConceptStr(# O,A #)] & O = { o where o is Object of C : g . o [= z } & A = { a where a is Attribute of C : z [= d . a } ) ;
consider z' being Element of L, O' being Subset of the carrier of C, A' being Subset of the carrier' of C such that
A76: ( [x,y2] = [z',ConceptStr(# O',A' #)] & O' = { o where o is Object of C : g . o [= z' } & A' = { a where a is Attribute of C : z' [= d . a } ) by A74;
z = [x,y1] `1 by A75, MCART_1:def 1
.= x by MCART_1:def 1
.= [x,y2] `1 by MCART_1:def 1
.= z' by A76, MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A75, A76, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis:

end;

then reconsider fi = fi as Function of the carrier of L,the carrier of (ConceptLattice C) by A73, FUNCT_1:def 1, FUNCT_2:def 1;
A77: for a, b being Element of L st a [= b holds
fi . a [= fi . b

proof

let a, b be Element of L; :: thesis:
assume A78: a [= b ; :: thesis:
A79: { o where o is Object of C : g . o [= a } c= { o where o is Object of C : g . o [= b }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { o where o is Object of C : g . o [= a } ; :: thesis:
then consider x' being Object of C such that
A80: ( x' = x & g . x' [= a ) ;
g . x' [= b by A78, A80, LATTICES:25;
hence x in { o where o is Object of C : g . o [= b } by A80; :: thesis:

end;

A81: dom fi = the carrier of L by FUNCT_2:def 1;
then consider ya being set such that
A82: [a,ya] in fi by RELAT_1:def 4;
consider xa being Element of L, Oa being Subset of the carrier of C, Aa being Subset of the carrier' of C such that
A83: ( [a,ya] = [xa,ConceptStr(# Oa,Aa #)] & Oa = { o where o is Object of C : g . o [= xa } & Aa = { a' where a' is Attribute of C : xa [= d . a' } ) by A82;
consider yb being set such that
A84: [b,yb] in fi by A81, RELAT_1:def 4;
consider xb being Element of L, Ob being Subset of the carrier of C, Ab being Subset of the carrier' of C such that
A85: ( [b,yb] = [xb,ConceptStr(# Ob,Ab #)] & Ob = { o where o is Object of C : g . o [= xb } & Ab = { a' where a' is Attribute of C : xb [= d . a' } ) by A84;
A86: a = [xa,ConceptStr(# Oa,Aa #)] `1 by A83, MCART_1:def 1
.= xa by MCART_1:def 1 ;
A87: b = [xb,ConceptStr(# Ob,Ab #)] `1 by A85, MCART_1:def 1
.= xb by MCART_1:def 1 ;
A88: fi . a = ConceptStr(# Oa,Aa #) by A82, A83, A86, FUNCT_1:8;
A89: fi . b = ConceptStr(# Ob,Ab #) by A84, A85, A87, FUNCT_1:8;
set ca = fi . a;
set cb = fi . b;
( the Extent of ((fi . a) @ ) = Oa & the Extent of ((fi . b) @ ) = Ob ) by A88, A89, CONLAT_1:def 24;
then (fi . a) @ is-SubConcept-of (fi . b) @ by A79, A83, A85, A86, A87, CONLAT_1:def 19;
hence fi . a [= fi . b by CONLAT_1:47; :: thesis:

end;

A90: for a being Element of L holds f . (fi . a) = a

proof

let a be Element of L; :: thesis:
reconsider a = a as Element of L ;
set O = { o where o is Object of C : g . o [= a } ;
{ o where o is Object of C : g . o [= a } c= the carrier of C

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { o where o is Object of C : g . o [= a } ; :: thesis:
then consider u' being Object of C such that
A91: ( u' = u & g . u' [= a ) ;
thus u in the carrier of C by A91; :: thesis:

end;

then reconsider O = { o where o is Object of C : g . o [= a } as Subset of the carrier of C ;
set A = { a' where a' is Attribute of C : a [= d . a' } ;
{ a' where a' is Attribute of C : a [= d . a' } c= the carrier' of C

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { a' where a' is Attribute of C : a [= d . a' } ; :: thesis:
then consider u' being Attribute of C such that
A92: ( u' = u & a [= d . u' ) ;
thus u in the carrier' of C by A92; :: thesis:

end;

then reconsider A = { a' where a' is Attribute of C : a [= d . a' } as Subset of the carrier' of C ;
A93: [a,ConceptStr(# O,A #)] in fi ;
set b = "\/" { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L;
ConceptStr(# O,A #) in rng fi by A93, RELAT_1:def 5;
then ConceptStr(# O,A #) is FormalConcept of C by A37, CONLAT_1:35;
then [ConceptStr(# O,A #),("\/" { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L)] in f ;
then A94: f . ConceptStr(# O,A #) = "\/" { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L by FUNCT_1:8;
"\/" { (g . o) where o is Object of C : o in { o' where o' is Object of C : g . o' [= a } } ,L = a

proof

consider D being Subset of (rng g) such that
A95: "\/" D,L = a by A28, LATTICE6:def 13;
A96: D is_less_than a by A95, LATTICE3:def 21;
D c= { (g . o) where o is Object of C : o in { o' where o' is Object of C : g . o' [= a } }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A97: u in D ; :: thesis:
then consider v being set such that
A98: ( v in dom g & u = g . v ) by FUNCT_1:def 5;
reconsider v = v as Object of C by A98;
g . v [= a by A96, A97, A98, LATTICE3:def 17;
then v in { o' where o' is Object of C : g . o' [= a } ;
hence u in { (g . o) where o is Object of C : o in { o' where o' is Object of C : g . o' [= a } } by A98; :: thesis:

end;

then A99: a [= "\/" { (g . o) where o is Object of C : o in { o' where o' is Object of C : g . o' [= a } } ,L by A95, LATTICE3:46;
{ (g . o) where o is Object of C : o in { o' where o' is Object of C : g . o' [= a } } is_less_than a

proof

let u be Element of L; :: according to LATTICE3:def 17 :: thesis:
assume u in { (g . o) where o is Object of C : o in { o' where o' is Object of C : g . o' [= a } } ; :: thesis:
then consider v being Object of C such that
A100: ( u = g . v & v in { o' where o' is Object of C : g . o' [= a } ) ;
consider ov being Object of C such that
A101: ( ov = v & g . ov [= a ) by A100;
thus u [= a by A100, A101; :: thesis:

end;

then "\/" { (g . o) where o is Object of C : o in { o' where o' is Object of C : g . o' [= a } } ,L [= a by LATTICE3:def 21;
hence "\/" { (g . o) where o is Object of C : o in { o' where o' is Object of C : g . o' [= a } } ,L = a by A99, LATTICES:26; :: thesis:

end;

hence f . (fi . a) = a by A93, A94, FUNCT_1:8; :: thesis:

end;

A102: for x being Element of (ConceptLattice C) holds f . x = "/\" { (d . a) where a is Attribute of C : a in the Intent of (x @ ) } ,L

proof

let x be Element of (ConceptLattice C); :: thesis:
set y = "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L;
A103: [(x @ ),("\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L)] in f ;
A104: f . x = f . (x @ ) by CONLAT_1:def 24
.= "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L by A103, FUNCT_1:8 ;
A105: for o' being Object of C st o' in the Extent of (x @ ) holds
for a' being Attribute of C st a' in the Intent of (x @ ) holds
g . o' [= d . a'

proof

let o' be Object of C; :: thesis:
assume A106: o' in the Extent of (x @ ) ; :: thesis:
let a' be Attribute of C; :: thesis:
assume a' in the Intent of (x @ ) ; :: thesis:
then a' in (ObjectDerivation C) . the Extent of (x @ ) by CONLAT_1:def 13;
then a' in { a where a is Attribute of C : for o being Object of C st o in the Extent of (x @ ) holds
o is-connected-with a } by CONLAT_1:def 6;
then consider aa being Attribute of C such that
A107: ( aa = a' & ( for o being Object of C st o in the Extent of (x @ ) holds
o is-connected-with aa ) ) ;
o' is-connected-with a' by A106, A107;
hence g . o' [= d . a' by A28; :: thesis:

end;

A108: for o being set st o in { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } holds
o in { (d . a) where a is Attribute of C : a in the Intent of (x @ ) }

proof

let o be set ; :: thesis:
assume o in { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } ; :: thesis:
then consider u being Attribute of C such that
A109: ( o = d . u & "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . u ) ;
A110: for o being Object of C st o in the Extent of (x @ ) holds
g . o [= d . u

proof

let o be Object of C; :: thesis:
assume o in the Extent of (x @ ) ; :: thesis:
then g . o in { (g . o') where o' is Object of C : o' in the Extent of (x @ ) } ;
then g . o [= "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L by LATTICE3:38;
hence g . o [= d . u by A109, LATTICES:25; :: thesis:

end;

for o being Object of C st o in the Extent of (x @ ) holds
o is-connected-with u

proof

let o be Object of C; :: thesis:
assume o in the Extent of (x @ ) ; :: thesis:
then g . o [= d . u by A110;
hence o is-connected-with u by A28; :: thesis:

end;

then u in { a' where a' is Attribute of C : for o' being Object of C st o' in the Extent of (x @ ) holds
o' is-connected-with a' } ;
then u in (ObjectDerivation C) . the Extent of (x @ ) by CONLAT_1:def 6;
then u in the Intent of (x @ ) by CONLAT_1:def 13;
hence o in { (d . a) where a is Attribute of C : a in the Intent of (x @ ) } by A109; :: thesis:

end;

A111: for o being set st o in { (d . a) where a is Attribute of C : a in the Intent of (x @ ) } holds
o in { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' }

proof

let o be set ; :: thesis:
assume o in { (d . a) where a is Attribute of C : a in the Intent of (x @ ) } ; :: thesis:
then consider b being Attribute of C such that
A112: ( o = d . b & b in the Intent of (x @ ) ) ;
{ (g . o') where o' is Object of C : o' in the Extent of (x @ ) } is_less_than d . b

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis:
assume q in { (g . o') where o' is Object of C : o' in the Extent of (x @ ) } ; :: thesis:
then consider u being Object of C such that
A113: ( q = g . u & u in the Extent of (x @ ) ) ;
thus q [= d . b by A105, A112, A113; :: thesis:

end;

then "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . b by LATTICE3:def 21;
hence o in { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } by A112; :: thesis:

end;

"/\" { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } ,L = "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L

proof

consider D being Subset of (rng d) such that
A114: "/\" D,L = "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L by A28, LATTICE6:def 14;
A115: "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L is_less_than D by A114, LATTICE3:34;
D c= { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A116: u in D ; :: thesis:
then consider v being set such that
A117: ( v in dom d & u = d . v ) by FUNCT_1:def 5;
reconsider v = v as Attribute of C by A117;
"\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . v by A115, A116, A117, LATTICE3:def 16;
hence u in { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } by A117; :: thesis:

end;

then A118: "/\" { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } ,L [= "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L by A114, LATTICE3:46;
"\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L is_less_than { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' }

proof

let u be Element of L; :: according to LATTICE3:def 16 :: thesis:
assume u in { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } ; :: thesis:
then consider v being Attribute of C such that
A119: ( u = d . v & "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . v ) ;
thus "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= u by A119; :: thesis:

end;

then "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= "/\" { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } ,L by LATTICE3:40;
hence "/\" { (d . a') where a' is Attribute of C : "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L [= d . a' } ,L = "\/" { (g . o) where o is Object of C : o in the Extent of (x @ ) } ,L by A118, LATTICES:26; :: thesis:

end;

hence f . x = "/\" { (d . a) where a is Attribute of C : a in the Intent of (x @ ) } ,L by A104, A108, A111, TARSKI:2; :: thesis:

end;

A120: for a being Element of (ConceptLattice C) holds fi . (f . a) = a

proof

let a be Element of (ConceptLattice C); :: thesis:
A121: fi . ("/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L) = fi . (f . a) by A102;
set x = "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L;
set O = { o where o is Object of C : g . o [= "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L } ;
{ o where o is Object of C : g . o [= "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L } c= the carrier of C

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { o where o is Object of C : g . o [= "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L } ; :: thesis:
then consider u' being Object of C such that
A122: ( u' = u & g . u' [= "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L ) ;
thus u in the carrier of C by A122; :: thesis:

end;

then reconsider O = { o where o is Object of C : g . o [= "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L } as Subset of the carrier of C ;
set A = { a' where a' is Attribute of C : "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L [= d . a' } ;
{ a' where a' is Attribute of C : "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L [= d . a' } c= the carrier' of C

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { a' where a' is Attribute of C : "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L [= d . a' } ; :: thesis:
then consider u' being Attribute of C such that
A123: ( u' = u & "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L [= d . u' ) ;
thus u in the carrier' of C by A123; :: thesis:

end;

then reconsider A = { a' where a' is Attribute of C : "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L [= d . a' } as Subset of the carrier' of C ;
[("/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L),ConceptStr(# O,A #)] in fi ;
then A124: fi . ("/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L) = ConceptStr(# O,A #) by FUNCT_1:8;
then A125: ConceptStr(# O,A #) is FormalConcept of C by A37, CONLAT_1:35;
A126: O = { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o [= d . a' }

proof

thus O c= { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o [= d . a' } :: according to XBOOLE_0:def 10 :: thesis:

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in O ; :: thesis:
then consider o' being Object of C such that
A127: ( u = o' & g . o' [= "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L ) ;
for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o' [= d . a'

proof

let a' be Attribute of C; :: thesis:
assume a' in the Intent of (a @ ) ; :: thesis:
then d . a' in { (d . y) where y is Attribute of C : y in the Intent of (a @ ) } ;
then "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L [= d . a' by LATTICE3:38;
hence g . o' [= d . a' by A127, LATTICES:25; :: thesis:

end;

hence u in { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o [= d . a' } by A127; :: thesis:

end;

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o [= d . a' } ; :: thesis:
then consider o' being Object of C such that
A128: ( o' = u & ( for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o' [= d . a' ) ) ;
g . o' is_less_than { (d . y) where y is Attribute of C : y in the Intent of (a @ ) }

proof

let q be Element of L; :: according to LATTICE3:def 16 :: thesis:
assume q in { (d . y) where y is Attribute of C : y in the Intent of (a @ ) } ; :: thesis:
then consider qa being Attribute of C such that
A129: ( q = d . qa & qa in the Intent of (a @ ) ) ;
thus g . o' [= q by A128, A129; :: thesis:

end;

then g . o' [= "/\" { (d . u) where u is Attribute of C : u in the Intent of (a @ ) } ,L by LATTICE3:34;
hence u in O by A128; :: thesis:

end;

{ o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o [= d . a' } = { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
o is-connected-with a' }

proof

thus { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o [= d . a' } c= { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
o is-connected-with a' } :: according to XBOOLE_0:def 10 :: thesis:

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o [= d . a' } ; :: thesis:
then consider u' being Object of C such that
A130: ( u = u' & ( for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . u' [= d . a' ) ) ;
for a' being Attribute of C st a' in the Intent of (a @ ) holds
u' is-connected-with a'

proof

let a' be Attribute of C; :: thesis:
assume a' in the Intent of (a @ ) ; :: thesis:
then g . u' [= d . a' by A130;
hence u' is-connected-with a' by A28; :: thesis:

end;

hence u in { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
o is-connected-with a' } by A130; :: thesis:

end;

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
o is-connected-with a' } ; :: thesis:
then consider u' being Object of C such that
A131: ( u = u' & ( for a' being Attribute of C st a' in the Intent of (a @ ) holds
u' is-connected-with a' ) ) ;
for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . u' [= d . a'

proof

let a' be Attribute of C; :: thesis:
assume a' in the Intent of (a @ ) ; :: thesis:
then u' is-connected-with a' by A131;
hence g . u' [= d . a' by A28; :: thesis:

end;

hence u in { o where o is Object of C : for a' being Attribute of C st a' in the Intent of (a @ ) holds
g . o [= d . a' } by A131; :: thesis:

end;

then A132: O = (AttributeDerivation C) . the Intent of (a @ ) by A126, CONLAT_1:def 7
.= the Extent of (a @ ) by CONLAT_1:def 13 ;
then A = (ObjectDerivation C) . the Extent of (a @ ) by A125, CONLAT_1:def 13
.= the Intent of (a @ ) by CONLAT_1:def 13 ;
hence fi . (f . a) = a by A121, A124, A132, CONLAT_1:def 24; :: thesis:

end;

A133: for a, b being Element of (ConceptLattice C) st f . a [= f . b holds
a [= b

proof

let a, b be Element of (ConceptLattice C); :: thesis:
assume A134: f . a [= f . b ; :: thesis:
( fi . (f . a) = a & fi . (f . b) = b ) by A120;
hence a [= b by A77, A134; :: thesis:

end;

then A135: f is one-to-one by Lm1;
the carrier of L c= rng f

proof

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume A136: u in the carrier of L ; :: thesis:
then u in dom fi by FUNCT_2:def 1;
then consider v being set such that
A137: [u,v] in fi by RELAT_1:def 4;
( rng fi c= the carrier of (ConceptLattice C) & v in rng fi ) by A137, RELAT_1:def 5;
then reconsider v = v as Element of (ConceptLattice C) ;
reconsider u = u as Element of L by A136;
A138: f . v = f . (fi . u) by A137, FUNCT_1:8
.= u by A90 ;
dom f = the carrier of (ConceptLattice C) by FUNCT_2:def 1;
hence u in rng f by A138, FUNCT_1:def 5; :: thesis:

end;

then A139: rng f = the carrier of L by XBOOLE_0:def 10;
then reconsider f = f as Homomorphism of ConceptLattice C,L by A38, A133, A135, Lm2;
A140: f is onto by A139, FUNCT_2:def 3;
f is one-to-one by A135;
then f is bijective by A140;
hence ConceptLattice C,L are_isomorphic by LATTICE4:def 5; :: thesis: