let L be complete Lattice; :: thesis: for C being FormalContext holds
( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C,the carrier of L ex d being Function of the carrier' of C,the carrier of L st
( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of
for a being Attribute of holds
( o is-connected-with a iff g . o [= d . a ) ) ) )
let C be FormalContext; :: thesis: ( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C,the carrier of L ex d being Function of the carrier' of C,the carrier of L st
( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of
for a being Attribute of holds
( o is-connected-with a iff g . o [= d . a ) ) ) )

hereby :: thesis: ( ex g being Function of the carrier of C,the carrier of L ex d being Function of the carrier' of C,the carrier of L st
( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of
for a being Attribute of holds
( o is-connected-with a iff g . o [= d . a ) ) ) implies ConceptLattice C,L are_isomorphic )

assume ConceptLattice C,L are_isomorphic ; :: thesis: ex g being Element of bool [:the carrier of C,the carrier of L:] ex d being Element of bool [:the carrier' of C,the carrier of L:] st
( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of
for a being Attribute of holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) )
then consider f being Homomorphism of ConceptLattice C,L such that
A1: f is bijective by LATTICE4:def 5;
take g = f * (gamma C); :: thesis: ex d being Element of bool [:the carrier' of C,the carrier of L:] st
( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of
for a being Attribute of holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) )
take d = f * (delta C); :: thesis: ( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of
for a being Attribute of holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) )
thus rng g is supremum-dense :: thesis: ( rng d is infimum-dense & ( for o being Object of
for a being Attribute of holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) )

proof

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

proof

let r be Element of ; :: thesis: ( { (f . x) where x is Element of : x in D' } is_less_than r implies a [= r )
consider r' being Element of such that
A5: r = f . r' by A1, LATTICE4:9;
reconsider r' = r' as Element of ;
assume A6: { (f . x) where x is Element of : x in D' } is_less_than r ; :: thesis: a [= r
for q being Element of st q in D' holds
q [= r'

proof

let q be Element of ; :: thesis: ( q in D' implies q [= r' )
assume q in D' ; :: thesis: q [= r'
then f . q in { (f . x) where x is Element of : x in D' } ;
then f . q [= f . r' by A6, A5, LATTICE3:def 17;
hence q [= r' by A1, LATTICE4:8; :: thesis: verum

end;

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

end;

A7: { (f . x) where x is Element of : x in D' } c= rng g

proof

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

end;

A12: D' is_less_than b by A3, LATTICE3:def 21;
{ (f . x) where x is Element of : x in D' } is_less_than a

proof

let q be Element of ; :: according to LATTICE3:def 17 :: thesis: ( not q in { (f . x) where x is Element of : x in D' } or q [= a )
assume q in { (f . x) where x is Element of : x in D' } ; :: thesis: q [= a
then consider q' being Element of such that
A13: q = f . q' and
A14: q' in D' ;
q' [= b by A12, A14, LATTICE3:def 17;
hence q [= a by A1, A2, A13, LATTICE4:8; :: thesis: verum

end;

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

end;

thus rng d is infimum-dense :: thesis: for o being Object of
for a being Attribute of holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) )

proof

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

proof

let r be Element of ; :: thesis: ( r is_less_than { (f . x) where x is Element of : x in D' } implies r [= a )
consider r' being Element of such that
A18: r = f . r' by A1, LATTICE4:9;
reconsider r' = r' as Element of ;
assume A19: r is_less_than { (f . x) where x is Element of : x in D' } ; :: thesis: r [= a
r' is_less_than D'

proof

let q be Element of ; :: according to LATTICE3:def 16 :: thesis: ( not q in D' or r' [= q )
assume q in D' ; :: thesis: r' [= q
then f . q in { (f . x) where x is Element of : x in D' } ;
then f . r' [= f . q by A19, A18, LATTICE3:def 16;
hence r' [= q by A1, LATTICE4:8; :: thesis: verum

end;

then r' [= b by A16, LATTICE3:34;
hence r [= a by A1, A15, A18, LATTICE4:8; :: thesis: verum

end;

A20: { (f . x) where x is Element of : x in D' } c= rng d

proof

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

end;

A25: b is_less_than D' by A16, LATTICE3:34;
a is_less_than { (f . x) where x is Element of : x in D' }

proof

let q be Element of ; :: according to LATTICE3:def 16 :: thesis: ( not q in { (f . x) where x is Element of : x in D' } or a [= q )
assume q in { (f . x) where x is Element of : x in D' } ; :: thesis: a [= q
then consider q' being Element of such that
A26: q = f . q' and
A27: q' in D' ;
b [= q' by A25, A27, LATTICE3:def 16;
hence a [= q by A1, A15, A26, LATTICE4:8; :: thesis: verum

end;

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

end;

let o be Object of ; :: thesis: for a being Attribute of holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) )
let a be Attribute of ; :: thesis: ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) )
A28: ( o is-connected-with a iff (gamma C) . o [= (delta C) . a ) by Th13;

hereby :: thesis: ( g . o [= d . a implies o is-connected-with a )

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

end;

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

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 A33: rng g is supremum-dense and
A34: rng d is infimum-dense and
A35: for o being Object of
for a being Attribute of holds
( o is-connected-with a iff g . o [= d . a ) ; :: thesis: ConceptLattice C,L are_isomorphic
set fi = { [x,ConceptStr(# O,A #)] where x is Element of , O is Subset of , A is Subset of : ( O = { o where o is Object of : g . o [= x } & A = { a where a is Attribute of : x [= d . a } ) } ;
set f = { [ConceptStr(# O,A #),x] where O is Subset of , A is Subset of , x is Element of : ( ConceptStr(# O,A #) is FormalConcept of & x = "\/" { (g . o) where o is Object of : o in O } ,L ) } ;
A36: ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 23;
A37: { [ConceptStr(# O,A #),x] where O is Subset of , A is Subset of , x is Element of : ( ConceptStr(# O,A #) is FormalConcept of & x = "\/" { (g . o) where o is Object of : 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: ( not y in { [ConceptStr(# O,A #),x] where O is Subset of , A is Subset of , x is Element of : ( ConceptStr(# O,A #) is FormalConcept of & x = "\/" { (g . o) where o is Object of : o in O } ,L ) } or y in [:the carrier of (ConceptLattice C),the carrier of L:] )
assume y in { [ConceptStr(# O,A #),x] where O is Subset of , A is Subset of , x is Element of : ( ConceptStr(# O,A #) is FormalConcept of & x = "\/" { (g . o) where o is Object of : o in O } ,L ) } ; :: thesis: y in [:the carrier of (ConceptLattice C),the carrier of L:]
then consider O being Subset of , A being Subset of , x being Element of such that
A38: y = [ConceptStr(# O,A #),x] and
A39: ConceptStr(# O,A #) is FormalConcept of and
x = "\/" { (g . o) where o is Object of : o in O } ,L ;
ConceptStr(# O,A #) in the carrier of (ConceptLattice C) by A36, A39, CONLAT_1:35;
hence y in [:the carrier of (ConceptLattice C),the carrier of L:] by A38, ZFMISC_1:def 2; :: thesis: verum

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { [x,ConceptStr(# O,A #)] where x is Element of , O is Subset of , A is Subset of : ( O = { o where o is Object of : g . o [= x } & A = { a where a is Attribute of : x [= d . a } ) } or y in [:the carrier of L,the carrier of (ConceptLattice C):] )
assume y in { [x,ConceptStr(# O,A #)] where x is Element of , O is Subset of , A is Subset of : ( O = { o where o is Object of : g . o [= x } & A = { a where a is Attribute of : x [= d . a } ) } ; :: thesis: y in [:the carrier of L,the carrier of (ConceptLattice C):]
then consider x being Element of , O being Subset of , A being Subset of such that
A40: y = [x,ConceptStr(# O,A #)] and
A41: O = { o where o is Object of : g . o [= x } and
A42: A = { a where a is Attribute of : x [= d . a } ;
A43: (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: the Extent of ConceptStr(# O,A #) c= (AttributeDerivation C) . the Intent of ConceptStr(# O,A #)

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) or u in the Extent of ConceptStr(# O,A #) )
A44: "/\" { (d . a') where a' is Attribute of : x [= d . a' } ,L = x

proof

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

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in D or u in { (d . a') where a' is Attribute of : x [= d . a' } )
assume A47: u in D ; :: thesis: u in { (d . a') where a' is Attribute of : x [= d . a' }
then consider v being set such that
A48: v in dom d and
A49: u = d . v by FUNCT_1:def 5;
reconsider v = v as Attribute of by A48;
x [= d . v by A46, A47, A49, LATTICE3:def 16;
hence u in { (d . a') where a' is Attribute of : x [= d . a' } by A49; :: thesis: verum

end;

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

proof

let u be Element of ; :: according to LATTICE3:def 16 :: thesis: ( not u in { (d . a') where a' is Attribute of : x [= d . a' } or x [= u )
assume u in { (d . a') where a' is Attribute of : x [= d . a' } ; :: thesis: x [= u
then ex v being Attribute of st
( u = d . v & x [= d . v ) ;
hence x [= u ; :: thesis: verum

end;

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

end;

assume u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) ; :: thesis: u in the Extent of ConceptStr(# O,A #)
then u in { o where o is Object of : for a being Attribute of 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 such that
A51: u' = u and
A52: for a being Attribute of st a in the Intent of ConceptStr(# O,A #) holds
u' is-connected-with a ;
A53: for v being Attribute of st v in { a where a is Attribute of : x [= d . a } holds
g . u' [= d . v

proof

let v be Attribute of ; :: thesis: ( v in { a where a is Attribute of : x [= d . a } implies g . u' [= d . v )
assume v in { a where a is Attribute of : x [= d . a } ; :: thesis: g . u' [= d . v
then u' is-connected-with v by A42, A52;
hence g . u' [= d . v by A35; :: thesis: verum

end;

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

proof

let q be Element of ; :: according to LATTICE3:def 16 :: thesis: ( not q in { (d . a) where a is Attribute of : x [= d . a } or g . u' [= q )
assume q in { (d . a) where a is Attribute of : x [= d . a } ; :: thesis: g . u' [= q
then consider b being Attribute of such that
A54: q = d . b and
A55: x [= d . b ;
b in { a where a is Attribute of : x [= d . a } by A55;
hence g . u' [= q by A53, A54; :: thesis: verum

end;

then g . u' [= x by A44, LATTICE3:34;
hence u in the Extent of ConceptStr(# O,A #) by A41, A51; :: thesis: verum

end;

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

proof

let v be Attribute of ; :: thesis: ( v in { a where a is Attribute of : x [= d . a } implies g . u' [= d . v )
assume v in { a where a is Attribute of : x [= d . a } ; :: thesis: g . u' [= d . v
then ex v' being Attribute of st
( v' = v & x [= d . v' ) ;
hence g . u' [= d . v by A57, LATTICES:25; :: thesis: verum

end;

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

proof

let v be Attribute of ; :: thesis: ( v in { a where a is Attribute of : x [= d . a } implies u' is-connected-with v )
assume v in { a where a is Attribute of : x [= d . a } ; :: thesis: u' is-connected-with v
then g . u' [= d . v by A58;
hence u' is-connected-with v by A35; :: thesis: verum

end;

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

end;

(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: the Intent of ConceptStr(# O,A #) c= (ObjectDerivation C) . the Extent of ConceptStr(# O,A #)

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) or u in the Intent of ConceptStr(# O,A #) )
A59: "\/" { (g . a') where a' is Object of : g . a' [= x } ,L = x

proof

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

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in D or u in { (g . a') where a' is Object of : g . a' [= x } )
assume A62: u in D ; :: thesis: u in { (g . a') where a' is Object of : g . a' [= x }
then consider v being set such that
A63: v in dom g and
A64: u = g . v by FUNCT_1:def 5;
reconsider v = v as Object of by A63;
g . v [= x by A61, A62, A64, LATTICE3:def 17;
hence u in { (g . a') where a' is Object of : g . a' [= x } by A64; :: thesis: verum

end;

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

proof

let u be Element of ; :: according to LATTICE3:def 17 :: thesis: ( not u in { (g . a') where a' is Object of : g . a' [= x } or u [= x )
assume u in { (g . a') where a' is Object of : g . a' [= x } ; :: thesis: u [= x
then ex v being Object of st
( u = g . v & g . v [= x ) ;
hence u [= x ; :: thesis: verum

end;

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

end;

assume u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) ; :: thesis: u in the Intent of ConceptStr(# O,A #)
then u in { o where o is Attribute of : for a being Object of 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 such that
A66: u' = u and
A67: for a being Object of st a in the Extent of ConceptStr(# O,A #) holds
a is-connected-with u' ;
A68: for v being Object of st v in { a where a is Object of : g . a [= x } holds
g . v [= d . u'

proof

let v be Object of ; :: thesis: ( v in { a where a is Object of : g . a [= x } implies g . v [= d . u' )
assume v in { a where a is Object of : g . a [= x } ; :: thesis: g . v [= d . u'
then v is-connected-with u' by A41, A67;
hence g . v [= d . u' by A35; :: thesis: verum

end;

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

proof

let q be Element of ; :: according to LATTICE3:def 17 :: thesis: ( not q in { (g . a) where a is Object of : g . a [= x } or q [= d . u' )
assume q in { (g . a) where a is Object of : g . a [= x } ; :: thesis: q [= d . u'
then consider b being Object of such that
A69: q = g . b and
A70: g . b [= x ;
b in { a where a is Object of : g . a [= x } by A70;
hence q [= d . u' by A68, A69; :: thesis: verum

end;

then x [= d . u' by A59, LATTICE3:def 21;
hence u in the Intent of ConceptStr(# O,A #) by A42, A66; :: thesis: verum

end;

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in the Intent of ConceptStr(# O,A #) or u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) )
assume u in the Intent of ConceptStr(# O,A #) ; :: thesis: u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #)
then consider u' being Attribute of such that
A71: u' = u and
A72: x [= d . u' by A42;
A73: for v being Object of st v in { a where a is Object of : g . a [= x } holds
g . v [= d . u'

proof

let v be Object of ; :: thesis: ( v in { a where a is Object of : g . a [= x } implies g . v [= d . u' )
assume v in { a where a is Object of : g . a [= x } ; :: thesis: g . v [= d . u'
then ex v' being Object of st
( v' = v & g . v' [= x ) ;
hence g . v [= d . u' by A72, LATTICES:25; :: thesis: verum

end;

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

proof

let v be Object of ; :: thesis: ( v in { a where a is Object of : g . a [= x } implies v is-connected-with u' )
assume v in { a where a is Object of : g . a [= x } ; :: thesis: v is-connected-with u'
then g . v [= d . u' by A73;
hence v is-connected-with u' by A35; :: thesis: verum

end;

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

end;

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

end;

then reconsider fi = { [x,ConceptStr(# O,A #)] where x is Element of , O is Subset of , A is Subset of : ( O = { o where o is Object of : g . o [= x } & A = { a where a is Attribute of : x [= d . a } ) } as Relation of , ;
A74: 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: ( [x,y1] in fi & [x,y2] in fi implies y1 = y2 )
assume that
A75: [x,y1] in fi and
A76: [x,y2] in fi ; :: thesis: y1 = y2
consider z being Element of , O being Subset of , A being Subset of such that
A77: [x,y1] = [z,ConceptStr(# O,A #)] and
A78: ( O = { o where o is Object of : g . o [= z } & A = { a where a is Attribute of : z [= d . a } ) by A75;
consider z' being Element of , O' being Subset of , A' being Subset of such that
A79: [x,y2] = [z',ConceptStr(# O',A' #)] and
A80: ( O' = { o where o is Object of : g . o [= z' } & A' = { a where a is Attribute of : z' [= d . a } ) by A76;
z = [x,y1] `1 by A77, MCART_1:def 1
.= x by MCART_1:def 1
.= [x,y2] `1 by MCART_1:def 1
.= z' by A79, MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A77, A78, A79, A80, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis: verum

end;

the carrier of L c= dom fi

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of L or y in dom fi )
assume y in the carrier of L ; :: thesis: y in dom fi
then reconsider y = y as Element of ;
set A = { a where a is Attribute of : y [= d . a } ;
{ a where a is Attribute of : y [= d . a } c= the carrier' of C

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { a where a is Attribute of : y [= d . a } or u in the carrier' of C )
assume u in { a where a is Attribute of : y [= d . a } ; :: thesis: u in the carrier' of C
then ex u' being Attribute of st
( u' = u & y [= d . u' ) ;
hence u in the carrier' of C ; :: thesis: verum

end;

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

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { o where o is Object of : g . o [= y } or u in the carrier of C )
assume u in { o where o is Object of : g . o [= y } ; :: thesis: u in the carrier of C
then ex u' being Object of st
( u' = u & g . u' [= y ) ;
hence u in the carrier of C ; :: thesis: verum

end;

then reconsider O = { o where o is Object of : g . o [= y } as Subset of ;
[y,ConceptStr(# O,A #)] in fi ;
hence y in dom fi by RELAT_1:def 4; :: thesis: verum

end;

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

proof

let y be set ; :: 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 A82: y is strict FormalConcept of strict by A36, CONLAT_1:35;
then consider O' being Subset of , A' being Subset of such that
A83: y = ConceptStr(# O',A' #) ;
reconsider z = "\/" { (g . o) where o is Object of : o in O' } ,L as Element of ;
[y,z] in f by A82, A83;
hence y in dom f by RELAT_1:def 4; :: thesis: verum

end;

then A84: the carrier of (ConceptLattice C) = dom f by XBOOLE_0:def 10;
reconsider fi = fi as Function of the carrier of L,the carrier of (ConceptLattice C) by A81, A74, FUNCT_1:def 1, FUNCT_2:def 1;
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: ( [x,y1] in f & [x,y2] in f implies y1 = y2 )
assume that
A85: [x,y1] in f and
A86: [x,y2] in f ; :: thesis: y1 = y2
consider O being Subset of , A being Subset of , z being Element of such that
A87: [x,y1] = [ConceptStr(# O,A #),z] and
ConceptStr(# O,A #) is FormalConcept of and
A88: z = "\/" { (g . o) where o is Object of : o in O } ,L by A85;
consider O' being Subset of , A' being Subset of , z' being Element of such that
A89: [x,y2] = [ConceptStr(# O',A' #),z'] and
ConceptStr(# O',A' #) is FormalConcept of and
A90: z' = "\/" { (g . o) where o is Object of : o in O' } ,L by A86;
ConceptStr(# O,A #) = [x,y1] `1 by A87, MCART_1:def 1
.= x by MCART_1:def 1
.= [x,y2] `1 by MCART_1:def 1
.= ConceptStr(# O',A' #) by A89, MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A87, A88, A89, A90, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis: verum

end;

then reconsider f = f as Function of the carrier of (ConceptLattice C),the carrier of L by A84, FUNCT_1:def 1, FUNCT_2:def 1;
A91: ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 23;
A92: for a being Element of holds f . (fi . a) = a

proof

let a be Element of ; :: thesis: f . (fi . a) = a
reconsider a = a as Element of ;
set A = { a' where a' is Attribute of : a [= d . a' } ;
{ a' where a' is Attribute of : a [= d . a' } c= the carrier' of C

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { a' where a' is Attribute of : a [= d . a' } or u in the carrier' of C )
assume u in { a' where a' is Attribute of : a [= d . a' } ; :: thesis: u in the carrier' of C
then ex u' being Attribute of st
( u' = u & a [= d . u' ) ;
hence u in the carrier' of C ; :: thesis: verum

end;

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

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { o where o is Object of : g . o [= a } or u in the carrier of C )
assume u in { o where o is Object of : g . o [= a } ; :: thesis: u in the carrier of C
then ex u' being Object of st
( u' = u & g . u' [= a ) ;
hence u in the carrier of C ; :: thesis: verum

end;

then reconsider O = { o where o is Object of : g . o [= a } as Subset of ;
set b = "\/" { (g . o) where o is Object of : o in the Extent of ConceptStr(# O,A #) } ,L;
A93: "\/" { (g . o) where o is Object of : o in { o' where o' is Object of : g . o' [= a } } ,L = a

proof

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

proof

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

end;

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

proof

let u be Element of ; :: according to LATTICE3:def 17 :: thesis: ( not u in { (g . o) where o is Object of : o in { o' where o' is Object of : g . o' [= a } } or u [= a )
assume u in { (g . o) where o is Object of : o in { o' where o' is Object of : g . o' [= a } } ; :: thesis: u [= a
then consider v being Object of such that
A100: u = g . v and
A101: v in { o' where o' is Object of : g . o' [= a } ;
ex ov being Object of st
( ov = v & g . ov [= a ) by A101;
hence u [= a by A100; :: thesis: verum

end;

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

end;

A102: [a,ConceptStr(# O,A #)] in fi ;
then ConceptStr(# O,A #) in rng fi by RELAT_1:def 5;
then ConceptStr(# O,A #) is FormalConcept of by A91, CONLAT_1:35;
then [ConceptStr(# O,A #),("\/" { (g . o) where o is Object of : o in the Extent of ConceptStr(# O,A #) } ,L)] in f ;
then f . ConceptStr(# O,A #) = "\/" { (g . o) where o is Object of : o in the Extent of ConceptStr(# O,A #) } ,L by FUNCT_1:8;
hence f . (fi . a) = a by A102, A93, FUNCT_1:8; :: thesis: verum

end;

the carrier of L c= rng f

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in the carrier of L or u in rng f )
A103: dom f = the carrier of (ConceptLattice C) by FUNCT_2:def 1;
assume A104: u in the carrier of L ; :: thesis: u in rng f
then u in dom fi by FUNCT_2:def 1;
then consider v being set such that
A105: [u,v] in fi by RELAT_1:def 4;
reconsider u = u as Element of by A104;
v in rng fi by A105, RELAT_1:def 5;
then reconsider v = v as Element of ;
f . v = f . (fi . u) by A105, FUNCT_1:8
.= u by A92 ;
hence u in rng f by A103, FUNCT_1:def 5; :: thesis: verum

end;

then A106: rng f = the carrier of L by XBOOLE_0:def 10;
A107: for x being Element of holds f . x = "/\" { (d . a) where a is Attribute of : a in the Intent of (x @ ) } ,L

proof

let x be Element of ; :: thesis: f . x = "/\" { (d . a) where a is Attribute of : a in the Intent of (x @ ) } ,L
set y = "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L;
A108: [(x @ ),("\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L)] in f ;
A109: for o being set st o in { (d . a') where a' is Attribute of : "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= d . a' } holds
o in { (d . a) where a is Attribute of : a in the Intent of (x @ ) }

proof

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

proof

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

end;

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

proof

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

end;

then u in { a' where a' is Attribute of : for o' being Object of 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 : a in the Intent of (x @ ) } by A110; :: thesis: verum

end;

A113: for o' being Object of st o' in the Extent of (x @ ) holds
for a' being Attribute of st a' in the Intent of (x @ ) holds
g . o' [= d . a'

proof

let o' be Object of ; :: thesis: ( o' in the Extent of (x @ ) implies for a' being Attribute of st a' in the Intent of (x @ ) holds
g . o' [= d . a' )
assume A114: o' in the Extent of (x @ ) ; :: thesis: for a' being Attribute of st a' in the Intent of (x @ ) holds
g . o' [= d . a'
let a' be Attribute of ; :: thesis: ( a' in the Intent of (x @ ) implies g . o' [= d . a' )
assume a' in the Intent of (x @ ) ; :: thesis: g . o' [= d . a'
then a' in (ObjectDerivation C) . the Extent of (x @ ) by CONLAT_1:def 13;
then a' in { a where a is Attribute of : for o being Object of st o in the Extent of (x @ ) holds
o is-connected-with a } by CONLAT_1:def 6;
then ex aa being Attribute of st
( aa = a' & ( for o being Object of st o in the Extent of (x @ ) holds
o is-connected-with aa ) ) ;
then o' is-connected-with a' by A114;
hence g . o' [= d . a' by A35; :: thesis: verum

end;

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

proof

let o be set ; :: thesis: ( o in { (d . a) where a is Attribute of : a in the Intent of (x @ ) } implies o in { (d . a') where a' is Attribute of : "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= d . a' } )
assume o in { (d . a) where a is Attribute of : a in the Intent of (x @ ) } ; :: thesis: o in { (d . a') where a' is Attribute of : "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= d . a' }
then consider b being Attribute of such that
A116: o = d . b and
A117: b in the Intent of (x @ ) ;
{ (g . o') where o' is Object of : o' in the Extent of (x @ ) } is_less_than d . b

proof

let q be Element of ; :: according to LATTICE3:def 17 :: thesis: ( not q in { (g . o') where o' is Object of : o' in the Extent of (x @ ) } or q [= d . b )
assume q in { (g . o') where o' is Object of : o' in the Extent of (x @ ) } ; :: thesis: q [= d . b
then ex u being Object of st
( q = g . u & u in the Extent of (x @ ) ) ;
hence q [= d . b by A113, A117; :: thesis: verum

end;

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

end;

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

proof

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

proof

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

end;

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

proof

let u be Element of ; :: according to LATTICE3:def 16 :: thesis: ( not u in { (d . a') where a' is Attribute of : "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= d . a' } or "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= u )
assume u in { (d . a') where a' is Attribute of : "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= d . a' } ; :: thesis: "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= u
then ex v being Attribute of st
( u = d . v & "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= d . v ) ;
hence "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L [= u ; :: thesis: verum

end;

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

end;

f . x = f . (x @ ) by CONLAT_1:def 24
.= "\/" { (g . o) where o is Object of : o in the Extent of (x @ ) } ,L by A108, FUNCT_1:8 ;
hence f . x = "/\" { (d . a) where a is Attribute of : a in the Intent of (x @ ) } ,L by A109, A115, A118, TARSKI:2; :: thesis: verum

end;

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

proof

let a be Element of ; :: thesis: fi . (f . a) = a
set x = "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L;
set A = { a' where a' is Attribute of : "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L [= d . a' } ;
{ a' where a' is Attribute of : "/\" { (d . u) where u is Attribute of : 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: ( not u in { a' where a' is Attribute of : "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L [= d . a' } or u in the carrier' of C )
assume u in { a' where a' is Attribute of : "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L [= d . a' } ; :: thesis: u in the carrier' of C
then ex u' being Attribute of st
( u' = u & "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L [= d . u' ) ;
hence u in the carrier' of C ; :: thesis: verum

end;

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

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { o where o is Object of : g . o [= "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L } or u in the carrier of C )
assume u in { o where o is Object of : g . o [= "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L } ; :: thesis: u in the carrier of C
then ex u' being Object of st
( u' = u & g . u' [= "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L ) ;
hence u in the carrier of C ; :: thesis: verum

end;

then reconsider O = { o where o is Object of : g . o [= "/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L } as Subset of ;
A126: O = { o where o is Object of : for a' being Attribute of st a' in the Intent of (a @ ) holds
g . o [= d . a' }

proof

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

proof

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

proof

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

end;

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

end;

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

proof

let q be Element of ; :: according to LATTICE3:def 16 :: thesis: ( not q in { (d . y) where y is Attribute of : y in the Intent of (a @ ) } or g . o' [= q )
assume q in { (d . y) where y is Attribute of : y in the Intent of (a @ ) } ; :: thesis: g . o' [= q
then ex qa being Attribute of st
( q = d . qa & qa in the Intent of (a @ ) ) ;
hence g . o' [= q by A130; :: thesis: verum

end;

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

end;

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

proof

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

proof

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

proof

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

end;

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

end;

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

proof

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

end;

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

end;

then A135: O = (AttributeDerivation C) . the Intent of (a @ ) by A126, CONLAT_1:def 7
.= the Extent of (a @ ) by CONLAT_1:def 13 ;
A136: fi . ("/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L) = fi . (f . a) by A107;
[("/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L),ConceptStr(# O,A #)] in fi ;
then A137: fi . ("/\" { (d . u) where u is Attribute of : u in the Intent of (a @ ) } ,L) = ConceptStr(# O,A #) by FUNCT_1:8;
then ConceptStr(# O,A #) is FormalConcept of by A91, CONLAT_1:35;
then A = (ObjectDerivation C) . the Extent of (a @ ) by A135, CONLAT_1:def 13
.= the Intent of (a @ ) by CONLAT_1:def 13 ;
hence fi . (f . a) = a by A136, A137, A135, CONLAT_1:def 24; :: thesis: verum

end;

A138: for a, b being Element of st a [= b holds
fi . a [= fi . b

proof

let a, b be Element of ; :: thesis: ( a [= b implies fi . a [= fi . b )
set ca = fi . a;
set cb = fi . b;
assume A139: a [= b ; :: thesis: fi . a [= fi . b
A140: { o where o is Object of : g . o [= a } c= { o where o is Object of : g . o [= b }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { o where o is Object of : g . o [= a } or x in { o where o is Object of : g . o [= b } )
assume x in { o where o is Object of : g . o [= a } ; :: thesis: x in { o where o is Object of : g . o [= b }
then consider x' being Object of such that
A141: x' = x and
A142: g . x' [= a ;
g . x' [= b by A139, A142, LATTICES:25;
hence x in { o where o is Object of : g . o [= b } by A141; :: thesis: verum

end;

A143: dom fi = the carrier of L by FUNCT_2:def 1;
then consider ya being set such that
A144: [a,ya] in fi by RELAT_1:def 4;
consider yb being set such that
A145: [b,yb] in fi by A143, RELAT_1:def 4;
consider xb being Element of , Ob being Subset of , Ab being Subset of such that
A146: [b,yb] = [xb,ConceptStr(# Ob,Ab #)] and
A147: Ob = { o where o is Object of : g . o [= xb } and
Ab = { a' where a' is Attribute of : xb [= d . a' } by A145;
A148: b = [xb,ConceptStr(# Ob,Ab #)] `1 by A146, MCART_1:def 1
.= xb by MCART_1:def 1 ;
then fi . b = ConceptStr(# Ob,Ab #) by A145, A146, FUNCT_1:8;
then A149: the Extent of ((fi . b) @ ) = Ob by CONLAT_1:def 24;
consider xa being Element of , Oa being Subset of , Aa being Subset of such that
A150: [a,ya] = [xa,ConceptStr(# Oa,Aa #)] and
A151: Oa = { o where o is Object of : g . o [= xa } and
Aa = { a' where a' is Attribute of : xa [= d . a' } by A144;
A152: a = [xa,ConceptStr(# Oa,Aa #)] `1 by A150, MCART_1:def 1
.= xa by MCART_1:def 1 ;
then fi . a = ConceptStr(# Oa,Aa #) by A144, A150, FUNCT_1:8;
then the Extent of ((fi . a) @ ) = Oa by CONLAT_1:def 24;
then (fi . a) @ is-SubConcept-of (fi . b) @ by A140, A151, A147, A152, A148, A149, CONLAT_1:def 19;
hence fi . a [= fi . b by CONLAT_1:47; :: thesis: verum

end;

A153: for a, b being Element of st f . a [= f . b holds
a [= b

proof

let a, b be Element of ; :: thesis: ( f . a [= f . b implies a [= b )
assume A154: f . a [= f . b ; :: thesis: a [= b
( fi . (f . a) = a & fi . (f . b) = b ) by A125;
hence a [= b by A138, A154; :: thesis: verum

end;

for a, b being Element of st a [= b holds
f . a [= f . b

proof

let a, b be Element of ; :: thesis: ( a [= b implies f . a [= f . b )
reconsider xa = "\/" { (g . o) where o is Object of : o in the Extent of (a @ ) } ,L, xb = "\/" { (g . o) where o is Object of : o in the Extent of (b @ ) } ,L as Element of ;
[(a @ ),xa] in f ;
then A155: f . (a @ ) = xa by FUNCT_1:8;
[(b @ ),xb] in f ;
then A156: f . (b @ ) = xb by FUNCT_1:8;
assume a [= b ; :: thesis: f . a [= f . b
then a @ is-SubConcept-of b @ by CONLAT_1:47;
then A157: the Extent of (a @ ) c= the Extent of (b @ ) by CONLAT_1:def 19;
A158: { (g . o) where o is Object of : o in the Extent of (a @ ) } c= { (g . o) where o is Object of : o in the Extent of (b @ ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (g . o) where o is Object of : o in the Extent of (a @ ) } or x in { (g . o) where o is Object of : o in the Extent of (b @ ) } )
assume x in { (g . o) where o is Object of : o in the Extent of (a @ ) } ; :: thesis: x in { (g . o) where o is Object of : o in the Extent of (b @ ) }
then ex o being Object of st
( x = g . o & o in the Extent of (a @ ) ) ;
hence x in { (g . o) where o is Object of : o in the Extent of (b @ ) } by A157; :: thesis: verum

end;

( a @ = a & b @ = b ) by CONLAT_1:def 24;
hence f . a [= f . b by A158, A155, A156, LATTICE3:46; :: thesis: verum

end;

then reconsider f = f as Homomorphism of ConceptLattice C,L by A153, A106, Lm1, Lm2;
A159: f is onto by A106, FUNCT_2:def 3;
f is one-to-one by A153, Lm1;
hence ConceptLattice C,L are_isomorphic by A159, LATTICE4:def 5; :: thesis: verum