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

proof

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

proof

let q be Element of (ConceptLattice C); :: thesis: ( q in D9 implies q [= r9 )
assume q in D9 ; :: thesis: q [= r9
then f . q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ;
then f . q [= f . r9 by A6, A5;
hence q [= r9 by A1, LATTICE4:5; :: thesis: verum

end;

then D9 is_less_than r9 ;
then b [= r9 by A3, LATTICE3:def 21;
hence a [= r by A1, A2, A5, LATTICE4:5; :: thesis: verum

end;

A7: { (f . x) where x is Element of (ConceptLattice C) : x in D9 } c= rng g

proof

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

end;

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

proof

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

end;

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

proof

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

proof

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

end;

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

end;

A20: { (f . x) where x is Element of (ConceptLattice C) : x in D9 } c= rng d

proof

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

end;

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

proof

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

end;

then a = "/\" ( { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ,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 C; :: thesis: for a being Attribute of C 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 C; :: 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:13;
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:13;
assume o is-connected-with a ; :: thesis: g . o [= d . a
hence g . o [= d . a by A1, A28, A30, A29, LATTICE4:5; :: 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:13;
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:13;
assume g . o [= d . a ; :: thesis: o is-connected-with a
then (gamma C) . o [= (delta C) . a by A1, A31, A32, LATTICE4:5;
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 C
for a being Attribute of C 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 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 } ) } ;
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) ) } ;
A36: ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 20;
A37: { [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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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) ) } or y in [: the carrier of (ConceptLattice C), the carrier of L:] )
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: y in [: the carrier of (ConceptLattice C), the carrier of L:]
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
A38: y = [ConceptStr(# O,A #),x] and
A39: ConceptStr(# O,A #) is FormalConcept of C and
x = "\/" ( { (g . o) where o is Object of C : o in O } ,L) ;
ConceptStr(# O,A #) in the carrier of (ConceptLattice C) by A36, A39, CONLAT_1:31;
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 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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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 } ) } or y in [: the carrier of L, the carrier of (ConceptLattice C):] )
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: y in [: the carrier of L, the carrier of (ConceptLattice C):]
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
A40: y = [x,ConceptStr(# O,A #)] and
A41: O = { o where o is Object of C : g . o [= x } and
A42: A = { a where a is Attribute of C : 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 object ; :: 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 . a9) where a9 is Attribute of C : x [= d . a9 } ,L) = x

proof

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

proof

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

end;

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

proof

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

end;

then x [= "/\" ( { (d . a9) where a9 is Attribute of C : x [= d . a9 } ,L) by LATTICE3:39;
hence "/\" ( { (d . a9) where a9 is Attribute of C : x [= d . a9 } ,L) = x by A50, LATTICES:8; :: 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 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 4;
then consider u9 being Object of C such that
A51: u9 = u and
A52: for a being Attribute of C st a in the Intent of ConceptStr(# O,A #) holds
u9 is-connected-with a ;
A53: for v being Attribute of C st v in { a where a is Attribute of C : x [= d . a } holds
g . u9 [= d . v by A35, A42, A52;
g . u9 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: ( not q in { (d . a) where a is Attribute of C : x [= d . a } or g . u9 [= q )
assume q in { (d . a) where a is Attribute of C : x [= d . a } ; :: thesis: g . u9 [= q
then consider b being Attribute of C such that
A54: q = d . b and
A55: x [= d . b ;
b in { a where a is Attribute of C : x [= d . a } by A55;
hence g . u9 [= q by A53, A54; :: thesis: verum

end;

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

end;

let u be object ; :: 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 u9 being Object of C such that
A56: u9 = u and
A57: g . u9 [= x by A41;
A58: for v being Attribute of C st v in { a where a is Attribute of C : x [= d . a } holds
g . u9 [= d . v

proof

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

end;

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

proof

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

end;

then u9 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 A42;
hence u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) by A56, CONLAT_1:def 4; :: 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 object ; :: 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 . a9) where a9 is Object of C : g . a9 [= x } ,L) = x

proof

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

proof

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

end;

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

proof

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

end;

then "\/" ( { (g . a9) where a9 is Object of C : g . a9 [= x } ,L) [= x by LATTICE3:def 21;
hence "\/" ( { (g . a9) where a9 is Object of C : g . a9 [= x } ,L) = x by A65, LATTICES:8; :: 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 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 3;
then consider u9 being Attribute of C such that
A66: u9 = u and
A67: for a being Object of C st a in the Extent of ConceptStr(# O,A #) holds
a is-connected-with u9 ;
A68: for v being Object of C st v in { a where a is Object of C : g . a [= x } holds
g . v [= d . u9 by A35, A41, A67;
{ (g . a) where a is Object of C : g . a [= x } is_less_than d . u9

proof

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

end;

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

end;

let u be object ; :: 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 u9 being Attribute of C such that
A71: u9 = u and
A72: x [= d . u9 by A42;
A73: for v being Object of C st v in { a where a is Object of C : g . a [= x } holds
g . v [= d . u9

proof

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

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 u9

proof

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

end;

then u9 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 A41;
hence u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) by A71, CONLAT_1:def 3; :: thesis: verum

end;

then ConceptStr(# O,A #) is FormalConcept of C by A43, Lm3, CONLAT_1:def 10;
then ConceptStr(# O,A #) in the carrier of (ConceptLattice C) by A36, CONLAT_1:31;
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 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) ;
A74: for x, y1, y2 being object st [x,y1] in fi & [x,y2] in fi holds
y1 = y2

proof

let x, y1, y2 be object ; :: 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 L, O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A77: [x,y1] = [z,ConceptStr(# O,A #)] and
A78: ( O = { o where o is Object of C : g . o [= z } & A = { a where a is Attribute of C : z [= d . a } ) by A75;
consider z9 being Element of L, O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A79: [x,y2] = [z9,ConceptStr(# O9,A9 #)] and
A80: ( O9 = { o where o is Object of C : g . o [= z9 } & A9 = { a where a is Attribute of C : z9 [= d . a } ) by A76;
A81: z = x by A77, XTUPLE_0:1
.= z9 by A79, XTUPLE_0:1 ;
thus y1 = [x,y1] `2
.= [x,y2] `2 by A77, A78, A79, A80, A81
.= y2 ; :: thesis: verum

end;

the carrier of L c= dom fi

proof

let y be object ; :: 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 L ;
set A = { a where a is Attribute of C : y [= d . a } ;
{ a where a is Attribute of C : y [= d . a } c= the carrier' of C

proof

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

end;

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

proof

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

end;

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

end;

then A82: the carrier of L = dom fi ;
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 by A37;
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 A83: y is strict FormalConcept of C by A36, CONLAT_1:31;
then consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A84: y = ConceptStr(# O9,A9 #) ;
reconsider z = "\/" ( { (g . o) where o is Object of C : o in O9 } ,L) as Element of L ;
[y,z] in f by A83, A84;
hence y in dom f by XTUPLE_0:def 12; :: thesis: verum

end;

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

end;

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

proof

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

proof

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

end;

then reconsider A = { a9 where a9 is Attribute of C : a [= d . a9 } as Subset of the carrier' of C ;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not u in { o where o is Object of C : g . o [= a } or u in the carrier of C )
assume u in { o where o is Object of C : g . o [= a } ; :: thesis: u in the carrier of C
then ex u9 being Object of C st
( u9 = u & g . u9 [= a ) ;
hence u in the carrier of C ; :: thesis: verum

end;

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

proof

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

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in D or u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } )
assume A98: u in D ; :: thesis: u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } }
then consider v being object such that
A99: v in dom g and
A100: u = g . v by FUNCT_1:def 3;
reconsider v = v as Object of C by A99;
g . v [= a by A97, A98, A100;
then v in { o9 where o9 is Object of C : g . o9 [= a } ;
hence u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } by A100; :: thesis: verum

end;

then A101: a [= "\/" ( { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } ,L) by A96, LATTICE3:45;
{ (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } is_less_than a

proof

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

end;

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

end;

A104: [a,ConceptStr(# O,A #)] in fi ;
then ConceptStr(# O,A #) in rng fi by XTUPLE_0:def 13;
then ConceptStr(# O,A #) is FormalConcept of C by A93, CONLAT_1:31;
then [ConceptStr(# O,A #),("\/" ( { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L))] in f ;
then f . ConceptStr(# O,A #) = "\/" ( { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L) by FUNCT_1:1;
hence f . (fi . a) = a by A104, A95, FUNCT_1:1; :: thesis: verum

end;

the carrier of L c= rng f

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in the carrier of L or u in rng f )
A105: dom f = the carrier of (ConceptLattice C) by FUNCT_2:def 1;
assume A106: 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 object such that
A107: [u,v] in fi by XTUPLE_0:def 12;
reconsider u = u as Element of L by A106;
v in rng fi by A107, XTUPLE_0:def 13;
then reconsider v = v as Element of (ConceptLattice C) ;
f . v = f . (fi . u) by A107, FUNCT_1:1
.= u by A94 ;
hence u in rng f by A105, FUNCT_1:def 3; :: thesis: verum

end;

then A108: rng f = the carrier of L ;
A109: 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: f . x = "/\" ( { (d . a) where a is Attribute of C : a in the Intent of (x @) } ,L)
set y = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L);
A110: [(x @),("\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L))] in f ;
A111: for o being object st o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } holds
o in { (d . a) where a is Attribute of C : a in the Intent of (x @) }

proof

let o be object ; :: thesis: ( o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } implies o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } )
assume o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ; :: thesis: o in { (d . a) where a is Attribute of C : a in the Intent of (x @) }
then consider u being Attribute of C such that
A112: o = d . u and
A113: "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . u ;
A114: 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: ( 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 . o9) where o9 is Object of C : o9 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 A113, LATTICES:7; :: thesis: verum

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: ( 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 A114;
hence o is-connected-with u by A35; :: thesis: verum

end;

then u in { a9 where a9 is Attribute of C : for o9 being Object of C st o9 in the Extent of (x @) holds
o9 is-connected-with a9 } ;
then u in (ObjectDerivation C) . the Extent of (x @) by CONLAT_1:def 3;
then u in the Intent of (x @) by CONLAT_1:def 10;
hence o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } by A112; :: thesis: verum

end;

A115: for o9 being Object of C st o9 in the Extent of (x @) holds
for a9 being Attribute of C st a9 in the Intent of (x @) holds
g . o9 [= d . a9

proof

let o9 be Object of C; :: thesis: ( o9 in the Extent of (x @) implies for a9 being Attribute of C st a9 in the Intent of (x @) holds
g . o9 [= d . a9 )
assume A116: o9 in the Extent of (x @) ; :: thesis: for a9 being Attribute of C st a9 in the Intent of (x @) holds
g . o9 [= d . a9
let a9 be Attribute of C; :: thesis: ( a9 in the Intent of (x @) implies g . o9 [= d . a9 )
assume a9 in the Intent of (x @) ; :: thesis: g . o9 [= d . a9
then a9 in (ObjectDerivation C) . the Extent of (x @) by CONLAT_1:def 10;
then a9 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 3;
then ex aa being Attribute of C st
( aa = a9 & ( for o being Object of C st o in the Extent of (x @) holds
o is-connected-with aa ) ) ;
then o9 is-connected-with a9 by A116;
hence g . o9 [= d . a9 by A35; :: thesis: verum

end;

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

proof

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

proof

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

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 . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } by A118; :: thesis: verum

end;

A120: "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,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
A121: "/\" (D,L) = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A34;
A122: "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) is_less_than D by A121, LATTICE3:34;
D c= { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 }

proof

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

end;

then A126: "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) [= "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A121, LATTICE3:45;
"\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) is_less_than { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 }

proof

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

end;

then "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) by LATTICE3:39;
hence "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A126, LATTICES:8; :: thesis: verum

end;

f . x = f . (x @) by CONLAT_1:def 21
.= "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A110, FUNCT_1:1 ;
hence f . x = "/\" ( { (d . a) where a is Attribute of C : a in the Intent of (x @) } ,L) by A111, A117, A120, TARSKI:2; :: thesis: verum

end;

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

proof

let a be Element of (ConceptLattice C); :: thesis: fi . (f . a) = a
set x = "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L);
set A = { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } ;
{ a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } c= the carrier' of C

proof

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

end;

then reconsider A = { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } as Subset of the carrier' of C ;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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) } or u in the carrier of C )
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: u in the carrier of C
then ex u9 being Object of C st
( u9 = u & g . u9 [= "/\" ( { (d . u) where u is Attribute of C : 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 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 ;
A128: O = { o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of (a @) holds
g . o [= d . a9 }

proof

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

proof

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

proof

let a9 be Attribute of C; :: thesis: ( a9 in the Intent of (a @) implies g . o9 [= d . a9 )
assume a9 in the Intent of (a @) ; :: thesis: g . o9 [= d . a9
then d . a9 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 . a9 by LATTICE3:38;
hence g . o9 [= d . a9 by A130, LATTICES:7; :: thesis: verum

end;

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

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of (a @) holds
g . o [= d . a9 } or u in O )
assume u in { o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of (a @) holds
g . o [= d . a9 } ; :: thesis: u in O
then consider o9 being Object of C such that
A131: o9 = u and
A132: for a9 being Attribute of C st a9 in the Intent of (a @) holds
g . o9 [= d . a9 ;
g . o9 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: ( not q in { (d . y) where y is Attribute of C : y in the Intent of (a @) } or g . o9 [= q )
assume q in { (d . y) where y is Attribute of C : y in the Intent of (a @) } ; :: thesis: g . o9 [= q
then ex qa being Attribute of C st
( q = d . qa & qa in the Intent of (a @) ) ;
hence g . o9 [= q by A132; :: thesis: verum

end;

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

end;

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

proof

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

proof

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

proof

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

end;

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

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of (a @) holds
o is-connected-with a9 } or u in { o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of (a @) holds
g . o [= d . a9 } )
assume u in { o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of (a @) holds
o is-connected-with a9 } ; :: thesis: u in { o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of (a @) holds
g . o [= d . a9 }
then consider u9 being Object of C such that
A135: u = u9 and
A136: for a9 being Attribute of C st a9 in the Intent of (a @) holds
u9 is-connected-with a9 ;
for a9 being Attribute of C st a9 in the Intent of (a @) holds
g . u9 [= d . a9 by A35, A136;
hence u in { o where o is Object of C : for a9 being Attribute of C st a9 in the Intent of (a @) holds
g . o [= d . a9 } by A135; :: thesis: verum

end;

then A137: O = (AttributeDerivation C) . the Intent of (a @) by A128, CONLAT_1:def 4
.= the Extent of (a @) by CONLAT_1:def 10 ;
A138: fi . ("/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L)) = fi . (f . a) by A109;
[("/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L)),ConceptStr(# O,A #)] in fi ;
then A139: fi . ("/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L)) = ConceptStr(# O,A #) by FUNCT_1:1;
then ConceptStr(# O,A #) is FormalConcept of C by A93, CONLAT_1:31;
then A = (ObjectDerivation C) . the Extent of (a @) by A137, CONLAT_1:def 10
.= the Intent of (a @) by CONLAT_1:def 10 ;
hence fi . (f . a) = a by A138, A139, A137, CONLAT_1:def 21; :: thesis: verum

end;

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

proof

let a, b be Element of L; :: thesis: ( a [= b implies fi . a [= fi . b )
set ca = fi . a;
set cb = fi . b;
assume A141: a [= b ; :: thesis: fi . a [= fi . b
A142: { 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in { o where o is Object of C : g . o [= a } or x in { o where o is Object of C : g . o [= b } )
assume x in { o where o is Object of C : g . o [= a } ; :: thesis: x in { o where o is Object of C : g . o [= b }
then consider x9 being Object of C such that
A143: x9 = x and
A144: g . x9 [= a ;
g . x9 [= b by A141, A144, LATTICES:7;
hence x in { o where o is Object of C : g . o [= b } by A143; :: thesis: verum

end;

A145: dom fi = the carrier of L by FUNCT_2:def 1;
then consider ya being object such that
A146: [a,ya] in fi by XTUPLE_0:def 12;
consider yb being object such that
A147: [b,yb] in fi by A145, XTUPLE_0:def 12;
consider xb being Element of L, Ob being Subset of the carrier of C, Ab being Subset of the carrier' of C such that
A148: [b,yb] = [xb,ConceptStr(# Ob,Ab #)] and
A149: Ob = { o where o is Object of C : g . o [= xb } and
Ab = { a9 where a9 is Attribute of C : xb [= d . a9 } by A147;
A150: b = [b,yb] `1
.= [xb,ConceptStr(# Ob,Ab #)] `1 by A148
.= xb ;
then fi . b = ConceptStr(# Ob,Ab #) by A147, A148, FUNCT_1:1;
then A151: the Extent of ((fi . b) @) = Ob by CONLAT_1:def 21;
consider xa being Element of L, Oa being Subset of the carrier of C, Aa being Subset of the carrier' of C such that
A152: [a,ya] = [xa,ConceptStr(# Oa,Aa #)] and
A153: Oa = { o where o is Object of C : g . o [= xa } and
Aa = { a9 where a9 is Attribute of C : xa [= d . a9 } by A146;
A154: a = [a,ya] `1
.= [xa,ConceptStr(# Oa,Aa #)] `1 by A152
.= xa ;
then fi . a = ConceptStr(# Oa,Aa #) by A146, A152, FUNCT_1:1;
then the Extent of ((fi . a) @) = Oa by CONLAT_1:def 21;
then (fi . a) @ is-SubConcept-of (fi . b) @ by A142, A153, A149, A154, A150, A151, CONLAT_1:def 16;
hence fi . a [= fi . b by CONLAT_1:43; :: thesis: verum

end;

A155: 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 )
assume A156: f . a [= f . b ; :: thesis: a [= b
( fi . (f . a) = a & fi . (f . b) = b ) by A127;
hence a [= b by A140, A156; :: thesis: verum

end;

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 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 ;
then A157: f . (a @) = xa by FUNCT_1:1;
[(b @),xb] in f ;
then A158: f . (b @) = xb by FUNCT_1:1;
assume a [= b ; :: thesis: f . a [= f . b
then a @ is-SubConcept-of b @ by CONLAT_1:43;
then A159: the Extent of (a @) c= the Extent of (b @) by CONLAT_1:def 16;
A160: { (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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (g . o) where o is Object of C : o in the Extent of (a @) } or x in { (g . o) where o is Object of C : o in the Extent of (b @) } )
assume x in { (g . o) where o is Object of C : o in the Extent of (a @) } ; :: thesis: x in { (g . o) where o is Object of C : o in the Extent of (b @) }
then ex o being Object of C st
( x = g . o & o in the Extent of (a @) ) ;
hence x in { (g . o) where o is Object of C : o in the Extent of (b @) } by A159; :: thesis: verum

end;

( a @ = a & b @ = b ) by CONLAT_1:def 21;
hence f . a [= f . b by A160, A157, A158, LATTICE3:45; :: thesis: verum

end;

then reconsider f = f as Homomorphism of (ConceptLattice C),L by A155, A108, Lm1, Lm2;
A161: f is onto by A108, FUNCT_2:def 3;
f is one-to-one by A155, Lm1;
hence ConceptLattice C,L are_isomorphic by A161, LATTICE4:def 3; :: thesis: verum