let L be complete Lattice; :: thesis: ConceptLattice (Context L),L are_isomorphic
reconsider g = id the carrier of L as Function of the carrier of (Context L),the carrier of L ;
reconsider d = id the carrier of L as Function of the carrier' of (Context L),the carrier of L ;
A1: rng g is supremum-dense

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
A2: "\/" {a},L = a by LATTICE3:43;
rng g = the carrier of L by RELAT_1:71;
hence ex b₁ being Element of bool (rng g) st a = "\/" b₁,L by A2; :: thesis: verum

end;

for a being Element of L ex D' being Subset of (rng d) st a = "/\" D',L

proof

let a be Element of L; :: thesis: ex D' being Subset of (rng d) st a = "/\" D',L
A3: "/\" {a},L = a by LATTICE3:43;
rng d = the carrier of L by RELAT_1:71;
hence ex D' being Subset of (rng d) st a = "/\" D',L by A3; :: thesis: verum

end;

then A4: rng d is infimum-dense by LATTICE6:def 14;
for o being Object of (Context L)
for a being Attribute of (Context L) holds
( o is-connected-with a iff g . o [= d . a )

proof

let o be Object of (Context L); :: thesis: for a being Attribute of (Context L) holds
( o is-connected-with a iff g . o [= d . a )
let a be Attribute of (Context L); :: thesis: ( o is-connected-with a iff g . o [= d . a )
reconsider o' = o, a' = a as Element of L ;
A5: ( o is-connected-with a iff [o,a] in the Information of (Context L) ) by CONLAT_1:def 5;
( g . o = o' & d . a = a' ) by FUNCT_1:34;
hence ( o is-connected-with a iff g . o [= d . a ) by A5, FILTER_1:32; :: thesis: verum

end;

hence ConceptLattice (Context L),L are_isomorphic by A1, A4, Th14; :: thesis: verum