set f = { [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } ;
A1: ConceptLattice (C .:) = LattStr(# (B-carrier (C .:)),(B-join (C .:)),(B-meet (C .:)) #) by CONLAT_1:def 20;
A2: ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 20;
then A3: (ConceptLattice C) .: = LattStr(# (B-carrier C),(B-meet C),(B-join C) #) by LATTICE2:def 2;
{ [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } c= [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } or y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] )
assume y in { [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } ; :: thesis: y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):]
then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A4: y = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] and
A5: ConceptStr(# O,A #) is FormalConcept of C ;
ConceptStr(# O,A #) .: is strict FormalConcept of C .: by A5;
then A6: ConceptStr(# O,A #) .: in the carrier of (ConceptLattice (C .:)) by A1, CONLAT_1:31;
ConceptStr(# O,A #) in the carrier of ((ConceptLattice C) .:) by A3, A5, CONLAT_1:31;
hence y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] by A4, A6, ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider f = { [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } as Relation of the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)) ;
the carrier of ((ConceptLattice C) .:) c= dom f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of ((ConceptLattice C) .:) or y in dom f )
assume y in the carrier of ((ConceptLattice C) .:) ; :: thesis: y in dom f
then A7: y is strict FormalConcept of C by A3, CONLAT_1:31;
then consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A8: y = ConceptStr(# O9,A9 #) ;
set z = ConceptStr(# O9,A9 #) .: ;
ConceptStr(# O9,A9 #) .: is strict FormalConcept of C .: by A7, A8;
then reconsider z = ConceptStr(# O9,A9 #) .: as Element of (ConceptLattice (C .:)) by A1, CONLAT_1:31;
[y,z] in f by A7, A8;
hence y in dom f by XTUPLE_0:def 12; :: thesis: verum

end;

then A9: the carrier of ((ConceptLattice C) .:) = dom f ;
for x, y1, y2 being object st [x,y1] in f & [x,y2] in f holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis: ( [x,y1] in f & [x,y2] in f implies y1 = y2 )
assume that
A10: [x,y1] in f and
A11: [x,y2] in f ; :: thesis: y1 = y2
consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A12: [x,y2] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] and
ConceptStr(# O9,A9 #) is FormalConcept of C by A11;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A13: [x,y1] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] and
ConceptStr(# O,A #) is FormalConcept of C by A10;
A14: ConceptStr(# O,A #) = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] `1
.= [x,y1] `1 by A13
.= x
.= [x,y2] `1
.= [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] `1 by A12
.= ConceptStr(# O9,A9 #) ;
thus y1 = [x,y1] `2
.= [x,y2] `2 by A13, A12, A14
.= y2 ; :: thesis: verum

end;

then reconsider f = f as Function of the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)) by A9, FUNCT_1:def 1, FUNCT_2:def 1;
A15: (ConceptLattice C) .: = LattStr(# the carrier of (ConceptLattice C), the L_meet of (ConceptLattice C), the L_join of (ConceptLattice C) #) by LATTICE2:def 2;
A16: 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: ( a [= b implies f . a [= f . b )
reconsider aa = a % , bb = b % as Element of (LattPOSet (ConceptLattice C)) by A15;
reconsider a9 = a, b9 = b as Element of (ConceptLattice C) by A15;
A17: dom f = the carrier of ((ConceptLattice C) .:) by FUNCT_2:def 1;
then consider fa being object such that
A18: [a,fa] in f by XTUPLE_0:def 12;
assume a [= b ; :: thesis: f . a [= f . b
then a % <= b % by LATTICE3:7;
then [(a %),(b %)] in the InternalRel of (LattPOSet ((ConceptLattice C) .:)) by ORDERS_2:def 5;
then [(a %),(b %)] in the InternalRel of (LattPOSet (ConceptLattice C)) ~ by LATTICE3:20;
then [(b %),(a %)] in the InternalRel of (LattPOSet (ConceptLattice C)) by RELAT_1:def 7;
then A19: bb <= aa by ORDERS_2:def 5;
( (% aa) % = aa & (% bb) % = bb ) ;
then % bb [= % aa by A19, LATTICE3:7;
then A20: (% bb) @ is-SubConcept-of (% aa) @ by CONLAT_1:43;
consider fb being object such that
A21: [b,fb] in f by A17, XTUPLE_0:def 12;
A22: fb in rng f by A21, XTUPLE_0:def 13;
A23: f . b = fb by A21, FUNCT_1:1;
consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A24: [b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] and
ConceptStr(# O9,A9 #) is FormalConcept of C by A21;
A25: b = [b,fb] `1
.= [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] `1 by A24
.= ConceptStr(# O9,A9 #) ;
A26: fa in rng f by A18, XTUPLE_0:def 13;
A27: f . a = fa by A18, FUNCT_1:1;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A28: [a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] and
ConceptStr(# O,A #) is FormalConcept of C by A18;
reconsider fa = fa as Element of (ConceptLattice (C .:)) by A26;
A29: a = [a,fa] `1
.= [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] `1 by A28
.= ConceptStr(# O,A #) ;
reconsider fb = fb as Element of (ConceptLattice (C .:)) by A22;
fb = [b,fb] `2
.= [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] `2 by A24
.= ConceptStr(# O9,A9 #) .: ;
then A30: the Intent of (fb @) = the Intent of (ConceptStr(# O9,A9 #) .:) by CONLAT_1:def 21
.= the Extent of ConceptStr(# O9,A9 #) by Def8
.= the Extent of (b9 @) by A25, CONLAT_1:def 21 ;
fa = [a,fa] `2
.= [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] `2 by A28
.= ConceptStr(# O,A #) .: ;
then the Intent of (fa @) = the Intent of (ConceptStr(# O,A #) .:) by CONLAT_1:def 21
.= the Extent of ConceptStr(# O,A #) by Def8
.= the Extent of (a9 @) by A29, CONLAT_1:def 21 ;
then the Intent of (fb @) c= the Intent of (fa @) by A20, A30, CONLAT_1:def 16;
then fa @ is-SubConcept-of fb @ by CONLAT_1:28;
hence f . a [= f . b by A27, A23, CONLAT_1:43; :: thesis: verum

end;

the carrier of (ConceptLattice (C .:)) c= rng f

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in the carrier of (ConceptLattice (C .:)) or u in rng f )
A31: dom f = the carrier of ((ConceptLattice C) .:) by FUNCT_2:def 1;
assume u in the carrier of (ConceptLattice (C .:)) ; :: thesis: u in rng f
then reconsider u = u as Element of (ConceptLattice (C .:)) ;
reconsider A9 = the Intent of (u @) as Subset of the carrier of C ;
reconsider O9 = the Extent of (u @) as Subset of the carrier' of C ;
set CP = ConceptStr(# A9,O9 #);
A32: ( not the Extent of (u @) is empty or not the Intent of (u @) is empty ) by CONLAT_1:def 8;
A33: (AttributeDerivation C) . the Intent of ConceptStr(# A9,O9 #) = (ObjectDerivation (C .:)) . the Extent of (u @) by Th19
.= the Extent of ConceptStr(# A9,O9 #) by CONLAT_1:def 10 ;
(ObjectDerivation C) . the Extent of ConceptStr(# A9,O9 #) = (AttributeDerivation (C .:)) . the Intent of (u @) by Th18
.= the Intent of ConceptStr(# A9,O9 #) by CONLAT_1:def 10 ;
then ConceptStr(# A9,O9 #) is FormalConcept of C by A33, A32, CONLAT_1:def 8, CONLAT_1:def 10;
then ConceptStr(# A9,O9 #) in dom f by A15, A2, A31, CONLAT_1:31;
then consider v being object such that
A34: [ConceptStr(# A9,O9 #),v] in f by XTUPLE_0:def 12;
consider Ov being Subset of the carrier of C, Av being Subset of the carrier' of C such that
A35: [ConceptStr(# A9,O9 #),v] = [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)] and
ConceptStr(# Ov,Av #) is FormalConcept of C by A34;
A36: ConceptStr(# A9,O9 #) = [ConceptStr(# A9,O9 #),v] `1
.= [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)] `1 by A35
.= ConceptStr(# Ov,Av #) ;
A37: v in rng f by A34, XTUPLE_0:def 13;
then reconsider v = v as strict FormalConcept of C .: by A1, CONLAT_1:31;
v = [ConceptStr(# A9,O9 #),v] `2
.= [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)] `2 by A35
.= ConceptStr(# Ov,Av #) .: ;
then ( the Extent of v = the Extent of (u @) & the Intent of v = the Intent of (u @) ) by A36, Def8;
hence u in rng f by A37, CONLAT_1:def 21; :: thesis: verum

end;

then A38: rng f = the carrier of (ConceptLattice (C .:)) ;
A39: f is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that
A40: a in dom f and
A41: b in dom f and
A42: f . a = f . b ; :: thesis: a = b
reconsider a = a, b = b as Element of ((ConceptLattice C) .:) by A40, A41;
consider fa being object such that
A43: [a,fa] in f by A40, XTUPLE_0:def 12;
consider fb being object such that
A44: [b,fb] in f by A41, XTUPLE_0:def 12;
A45: f . b = fb by A44, FUNCT_1:1;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A46: [a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] and
ConceptStr(# O,A #) is FormalConcept of C by A43;
A47: a = ConceptStr(# O,A #) by A46, XTUPLE_0:1;
consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A48: [b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] and
ConceptStr(# O9,A9 #) is FormalConcept of C by A44;
A49: b = ConceptStr(# O9,A9 #) by A48, XTUPLE_0:1;
A50: ConceptStr(# O9,A9 #) .: = fb by A48, XTUPLE_0:1
.= fa by A42, A43, A45, FUNCT_1:1
.= ConceptStr(# O,A #) .: by A46, XTUPLE_0:1 ;
then A51: the Intent of ConceptStr(# O9,A9 #) = the Extent of (ConceptStr(# O,A #) .:) by Def8
.= the Intent of ConceptStr(# O,A #) by Def8 ;
the Extent of ConceptStr(# O9,A9 #) = the Intent of (ConceptStr(# O,A #) .:) by A50, Def8
.= the Extent of ConceptStr(# O,A #) by Def8 ;
hence a = b by A47, A49, A51; :: thesis: verum

end;

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: ( f . a [= f . b implies a [= b )
A52: dom f = the carrier of ((ConceptLattice C) .:) by FUNCT_2:def 1;
then consider fa being object such that
A53: [a,fa] in f by XTUPLE_0:def 12;
reconsider a9 = a, b9 = b as Element of (ConceptLattice C) by A15;
assume f . a [= f . b ; :: thesis: a [= b
then A54: (f . a) @ is-SubConcept-of (f . b) @ by CONLAT_1:43;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A55: [a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] and
ConceptStr(# O,A #) is FormalConcept of C by A53;
A56: a = ConceptStr(# O,A #) by A55, XTUPLE_0:1;
A57: fa in rng f by A53, XTUPLE_0:def 13;
consider fb being object such that
A58: [b,fb] in f by A52, XTUPLE_0:def 12;
A59: fb in rng f by A58, XTUPLE_0:def 13;
consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A60: [b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] and
ConceptStr(# O9,A9 #) is FormalConcept of C by A58;
A61: b = ConceptStr(# O9,A9 #) by A60, XTUPLE_0:1;
reconsider fb = fb as Element of (ConceptLattice (C .:)) by A59;
A62: fb = ConceptStr(# O9,A9 #) .: by A60, XTUPLE_0:1;
A63: the Intent of ((f . b) @) = the Intent of (fb @) by A58, FUNCT_1:1
.= the Intent of (ConceptStr(# O9,A9 #) .:) by A62, CONLAT_1:def 21
.= the Extent of ConceptStr(# O9,A9 #) by Def8
.= the Extent of (b9 @) by A61, CONLAT_1:def 21 ;
reconsider fa = fa as Element of (ConceptLattice (C .:)) by A57;
A64: fa = ConceptStr(# O,A #) .: by A55, XTUPLE_0:1;
the Intent of ((f . a) @) = the Intent of (fa @) by A53, FUNCT_1:1
.= the Intent of (ConceptStr(# O,A #) .:) by A64, CONLAT_1:def 21
.= the Extent of ConceptStr(# O,A #) by Def8
.= the Extent of (a9 @) by A56, CONLAT_1:def 21 ;
then the Extent of (b9 @) c= the Extent of (a9 @) by A54, A63, CONLAT_1:28;
then b9 @ is-SubConcept-of a9 @ by CONLAT_1:def 16;
then b9 [= a9 by CONLAT_1:43;
then b9 % <= a9 % by LATTICE3:7;
then [(b9 %),(a9 %)] in the InternalRel of (LattPOSet (ConceptLattice C)) by ORDERS_2:def 5;
then [(a %),(b %)] in the InternalRel of ((LattPOSet (ConceptLattice C)) ~) by RELAT_1:def 7;
then [(a %),(b %)] in the InternalRel of (LattPOSet ((ConceptLattice C) .:)) by LATTICE3:20;
then a % <= b % by ORDERS_2:def 5;
hence a [= b by LATTICE3:7; :: thesis: verum

end;

then reconsider f = f as Homomorphism of ((ConceptLattice C) .:),(ConceptLattice (C .:)) by A16, A38, A39, Lm2;
for CP being strict FormalConcept of C holds f . CP = CP .:

proof

let CP be strict FormalConcept of C; :: thesis: f . CP = CP .:
CP in B-carrier C by CONLAT_1:31;
then CP in dom f by A3, FUNCT_2:def 1;
then consider v being object such that
A65: [CP,v] in f by XTUPLE_0:def 12;
A66: v in rng f by A65, XTUPLE_0:def 13;
consider Ov being Subset of the carrier of C, Av being Subset of the carrier' of C such that
A67: [CP,v] = [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)] and
ConceptStr(# Ov,Av #) is FormalConcept of C by A65;
reconsider v = v as strict FormalConcept of C .: by A1, A66, CONLAT_1:31;
A68: CP = ConceptStr(# Ov,Av #) by A67, XTUPLE_0:1;
v = ConceptStr(# Ov,Av #) .: by A67, XTUPLE_0:1;
hence f . CP = CP .: by A65, A68, FUNCT_1:1; :: thesis: verum

end;

hence ex b₁ being Homomorphism of ((ConceptLattice C) .:),(ConceptLattice (C .:)) st
for CP being strict FormalConcept of C holds b₁ . CP = CP .: ; :: thesis: verum