let L be complete Lattice; :: thesis:
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: 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 )

let o be Object of (Context L); :: thesis:
let a be Attribute of (Context L); :: thesis:
reconsider o9 = o, a9 = a as Element of L ;
( o is-connected-with a iff [o,a] in the Information of (Context L) ) by CONLAT_1:def 2;
hence ( o is-connected-with a iff g . o [= d . a ) by FILTER_1:31; :: thesis:

end;

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

let a be Element of L; :: thesis:
( "/\" ({a},L) = a & rng d = the carrier of L ) by LATTICE3:42, RELAT_1:45;
hence ex D9 being Subset of (rng d) st a = "/\" (D9,L) ; :: thesis:

end;

then A2: rng d is infimum-dense ;
rng g is supremum-dense

let a be Element of L; :: according to LATTICE6:def 13 :: thesis:
( "\/" ({a},L) = a & rng g = the carrier of L ) by LATTICE3:42, RELAT_1:45;
hence ex b₁ being Element of bool (rng g) st a = "\/" (b₁,L) ; :: thesis:

end;

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