let L be Lattice; :: thesis: ( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic )

hereby :: thesis: ( ex C being FormalContext st ConceptLattice C,L are_isomorphic implies L is complete )

assume L is complete ; :: thesis: ex C being FormalContext st ConceptLattice C,L are_isomorphic
then ConceptLattice (Context L),L are_isomorphic by Th15;
hence ex C being FormalContext st ConceptLattice C,L are_isomorphic ; :: thesis: verum

end;

given C being FormalContext such that A1: ConceptLattice C,L are_isomorphic ; :: thesis: L is complete
consider f being Homomorphism of L, ConceptLattice C such that
A2: f is bijective by A1, LATTICE4:def 5;
let X be Subset of L; :: according to VECTSP_8:def 6 :: thesis: ex b₁ being Element of the carrier of L st
( b₁ is_less_than X & ( for b₂ being Element of the carrier of L holds
( not b₂ is_less_than X or b₂ [= b₁ ) ) )
set FX = { (f . x) where x is Element of L : x in X } ;
{ (f . x) where x is Element of L : x in X } c= the carrier of (ConceptLattice C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . x) where x is Element of L : x in X } or x in the carrier of (ConceptLattice C) )
assume x in { (f . x) where x is Element of L : x in X } ; :: thesis: x in the carrier of (ConceptLattice C)
then consider y being Element of L such that
A3: ( x = f . y & y in X ) ;
thus x in the carrier of (ConceptLattice C) by A3; :: thesis: verum

end;

then reconsider FX = { (f . x) where x is Element of L : x in X } as Subset of (ConceptLattice C) ;
set Fa = "/\" FX,(ConceptLattice C);
A4: ( "/\" FX,(ConceptLattice C) is_less_than FX & ( for b being Element of (ConceptLattice C) st b is_less_than FX holds
b [= "/\" FX,(ConceptLattice C) ) ) by LATTICE3:34;
A5: ( f is onto & f is one-to-one ) by A2;
then consider a being Element of L such that
A6: "/\" FX,(ConceptLattice C) = f . a by LATTICE4:9;
A7: a is_less_than X

proof

let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not q in X or a [= q )
assume q in X ; :: thesis: a [= q
then f . q in FX ;
then "/\" FX,(ConceptLattice C) [= f . q by A4, LATTICE3:def 16;
hence a [= q by A5, A6, LATTICE4:8; :: thesis: verum

end;

for b being Element of L st b is_less_than X holds
b [= a

proof

let b be Element of L; :: thesis: ( b is_less_than X implies b [= a )
assume A8: b is_less_than X ; :: thesis: b [= a
f . b is_less_than FX

proof

let q be Element of (ConceptLattice C); :: according to LATTICE3:def 16 :: thesis: ( not q in FX or f . b [= q )
assume q in FX ; :: thesis: f . b [= q
then consider y being Element of L such that
A9: ( q = f . y & y in X ) ;
b [= y by A8, A9, LATTICE3:def 16;
hence f . b [= q by A5, A9, LATTICE4:8; :: thesis: verum

end;

then f . b [= f . a by A6, LATTICE3:34;
hence b [= a by A5, LATTICE4:8; :: thesis: verum

end;

hence ex b₁ being Element of the carrier of L st
( b₁ is_less_than X & ( for b₂ being Element of the carrier of L holds
( not b₂ is_less_than X or b₂ [= b₁ ) ) ) by A7; :: thesis: verum