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
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₁ ) ) )
consider f being Homomorphism of L,(ConceptLattice C) such that
A2: f is bijective by A1, LATTICE4:def 3;
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 object ; :: 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 ex y being Element of L st
( x = f . y & y in X ) ;
hence x in the carrier of (ConceptLattice C) ; :: 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));
consider a being Element of L such that
A3: "/\" (FX,(ConceptLattice C)) = f . a by A2, LATTICE4:6;
A4: 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 A5: 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
A6: q = f . y and
A7: y in X ;
b [= y by A5, A7;
hence f . b [= q by A2, A6, LATTICE4:5; :: thesis: verum

end;

then f . b [= f . a by A3, LATTICE3:34;
hence b [= a by A2, LATTICE4:5; :: thesis: verum

end;

A8: "/\" (FX,(ConceptLattice C)) is_less_than FX by LATTICE3:34;
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 A8;
hence a [= q by A2, A3, LATTICE4:5; :: 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 A4; :: thesis: verum