let C be FormalContext; :: thesis: ConceptLattice C is complete Lattice
for X being Subset of (ConceptLattice C) ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) )

proof

let X be Subset of (ConceptLattice C); :: thesis: ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) )

per cases ( X = {} or X <> {} ) ;

suppose A1: X = {} ; :: thesis: ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) )

A2: for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= Top (ConceptLattice C)

proof

let b be Element of (ConceptLattice C); :: thesis: ( b is_less_than X implies b [= Top (ConceptLattice C) )
assume b is_less_than X ; :: thesis: b [= Top (ConceptLattice C)
ex c being Element of (ConceptLattice C) st
for a being Element of (ConceptLattice C) holds
( c "\/" a = c & a "\/" c = c )

proof

reconsider CO = Concept-with-all-Objects C as Element of (ConceptLattice C) by Th31;
for CP being Element of (ConceptLattice C) holds
( CO "\/" CP = CO & CP "\/" CO = CO )

proof

let CP be Element of (ConceptLattice C); :: thesis: ( CO "\/" CP = CO & CP "\/" CO = CO )
reconsider CP = CP as strict FormalConcept of C by Th31;
reconsider CO = CO as strict FormalConcept of C ;
(B-join C) . (CO,CP) = (B-join C) . (CP,CO) by Th33
.= CO by Th39 ;
hence ( CO "\/" CP = CO & CP "\/" CO = CO ) by LATTICES:def 1; :: thesis: verum

end;

hence ex c being Element of (ConceptLattice C) st
for a being Element of (ConceptLattice C) holds
( c "\/" a = c & a "\/" c = c ) ; :: thesis: verum

end;

then ConceptLattice C is upper-bounded by LATTICES:def 14;
then (Top (ConceptLattice C)) "\/" b = Top (ConceptLattice C) ;
hence b [= Top (ConceptLattice C) by LATTICES:def 3; :: thesis: verum

end;

for q being Element of (ConceptLattice C) st q in X holds
Top (ConceptLattice C) [= q by A1;
then Top (ConceptLattice C) is_less_than X by LATTICE3:def 16;
hence ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) ) by A2; :: thesis: verum

end;

suppose X <> {} ; :: thesis: ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) )

then reconsider X = X as non empty Subset of (ConceptLattice C) ;
set ExX = { the Extent of x where x is Element of B-carrier C : x in X } ;
A3: for x being Element of X holds the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X }

proof

let x be Element of X; :: thesis: the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X }
x in X ;
then reconsider x = x as Element of B-carrier C ;
the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X } ;
hence the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X } ; :: thesis: verum

end;

then reconsider ExX = { the Extent of x where x is Element of B-carrier C : x in X } as non empty set ;
set E1 = meet ExX;
A4: for o being Object of C holds
( o in meet ExX iff for x being Element of X holds o in the Extent of x )

proof

let o be Object of C; :: thesis: ( o in meet ExX iff for x being Element of X holds o in the Extent of x )
A5: ( ( for x being Element of X holds o in the Extent of x ) implies o in meet ExX )

proof

assume A6: for x being Element of X holds o in the Extent of x ; :: thesis: o in meet ExX
for Y being set st Y in ExX holds
o in Y

proof

let Y be set ; :: thesis: ( Y in ExX implies o in Y )
assume Y in ExX ; :: thesis: o in Y
then ex Y9 being Element of B-carrier C st
( Y = the Extent of Y9 & Y9 in X ) ;
hence o in Y by A6; :: thesis: verum

end;

hence o in meet ExX by SETFAM_1:def 1; :: thesis: verum

end;

( o in meet ExX implies for x being Element of X holds o in the Extent of x )

proof

assume A7: o in meet ExX ; :: thesis: for x being Element of X holds o in the Extent of x
let x be Element of X; :: thesis: o in the Extent of x
the Extent of x in ExX by A3;
hence o in the Extent of x by A7, SETFAM_1:def 1; :: thesis: verum

end;

hence ( o in meet ExX iff for x being Element of X holds o in the Extent of x ) by A5; :: thesis: verum

end;

meet ExX c= the carrier of C

proof

set Y = the Element of ExX;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet ExX or x in the carrier of C )
the Element of ExX in ExX ;
then consider Y9 being Element of B-carrier C such that
A8: the Element of ExX = the Extent of Y9 and
Y9 in X ;
assume x in meet ExX ; :: thesis: x in the carrier of C
then x in the Extent of Y9 by A8, SETFAM_1:def 1;
hence x in the carrier of C ; :: thesis: verum

end;

then consider O being Subset of the carrier of C such that
A9: for o being Object of C holds
( o in O iff for x being Element of X holds o in the Extent of x ) by A4;
set InX = { the Intent of x where x is Element of B-carrier C : x in X } ;
set In = union { the Intent of x where x is Element of B-carrier C : x in X } ;
A10: for a being Attribute of C holds
( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x )

proof

let a be Attribute of C; :: thesis: ( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x )
A11: ( ex x being Element of X st a in the Intent of x implies a in union { the Intent of x where x is Element of B-carrier C : x in X } )

proof

assume A12: ex x being Element of X st a in the Intent of x ; :: thesis: a in union { the Intent of x where x is Element of B-carrier C : x in X }
ex Y being set st
( a in Y & Y in { the Intent of x where x is Element of B-carrier C : x in X } )

proof

consider x being Element of X such that
A13: a in the Intent of x by A12;
x in X ;
then the Intent of x in { the Intent of x where x is Element of B-carrier C : x in X } ;
hence ex Y being set st
( a in Y & Y in { the Intent of x where x is Element of B-carrier C : x in X } ) by A13; :: thesis: verum

end;

hence a in union { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def 4; :: thesis: verum

end;

( a in union { the Intent of x where x is Element of B-carrier C : x in X } implies ex x being Element of X st a in the Intent of x )

proof

assume a in union { the Intent of x where x is Element of B-carrier C : x in X } ; :: thesis: ex x being Element of X st a in the Intent of x
then consider Y being set such that
A14: a in Y and
A15: Y in { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def 4;
ex Y9 being Element of B-carrier C st
( Y = the Intent of Y9 & Y9 in X ) by A15;
hence ex x being Element of X st a in the Intent of x by A14; :: thesis: verum

end;

hence ( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x ) by A11; :: thesis: verum

end;

union { the Intent of x where x is Element of B-carrier C : x in X } c= the carrier' of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { the Intent of x where x is Element of B-carrier C : x in X } or x in the carrier' of C )
assume x in union { the Intent of x where x is Element of B-carrier C : x in X } ; :: thesis: x in the carrier' of C
then consider Y being set such that
A16: x in Y and
A17: Y in { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def 4;
ex Y9 being Element of B-carrier C st
( Y = the Intent of Y9 & Y9 in X ) by A17;
hence x in the carrier' of C by A16; :: thesis: verum

end;

then consider A9 being Subset of the carrier' of C such that
A18: for a being Attribute of C holds
( a in A9 iff ex x being Element of X st a in the Intent of x ) by A10;
A19: for o being Object of C holds
( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x )

proof

let o be Object of C; :: thesis: ( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x )
A20: ( ( for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ) implies o in O )

proof

assume A21: for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ; :: thesis: o in O
for x being Element of X holds o in the Extent of x

proof

let x be Element of X; :: thesis: o in the Extent of x
o in (AttributeDerivation C) . the Intent of x by A21;
hence o in the Extent of x by Def9; :: thesis: verum

end;

hence o in O by A9; :: thesis: verum

end;

( o in O implies for x being Element of X holds o in (AttributeDerivation C) . the Intent of x )

proof

assume A22: o in O ; :: thesis: for x being Element of X holds o in (AttributeDerivation C) . the Intent of x
for x being Element of X holds o in (AttributeDerivation C) . the Intent of x

proof

let x be Element of X; :: thesis: o in (AttributeDerivation C) . the Intent of x
o in the Extent of x by A9, A22;
hence o in (AttributeDerivation C) . the Intent of x by Def9; :: thesis: verum

end;

hence for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ; :: thesis: verum

end;

hence ( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ) by A20; :: thesis: verum

end;

A23: for x being object st x in (AttributeDerivation C) . A9 holds
x in O

proof

let x be object ; :: thesis: ( x in (AttributeDerivation C) . A9 implies x in O )
assume x in (AttributeDerivation C) . A9 ; :: thesis: x in O
then x in { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } by Def3;
then consider x9 being Object of C such that
A24: x9 = x and
A25: for a being Attribute of C st a in A9 holds
x9 is-connected-with a ;
for x being Element of X holds x9 in (AttributeDerivation C) . the Intent of x

proof

let x be Element of X; :: thesis: x9 in (AttributeDerivation C) . the Intent of x
for a being Attribute of C st a in the Intent of x holds
x9 is-connected-with a by A18, A25;
then x9 in { o where o is Object of C : for a being Attribute of C st a in the Intent of x holds
o is-connected-with a } ;
hence x9 in (AttributeDerivation C) . the Intent of x by Def3; :: thesis: verum

end;

hence x in O by A19, A24; :: thesis: verum

end;

consider A being Subset of the carrier' of C such that
A26: A = (ObjectDerivation C) . ((AttributeDerivation C) . A9) ;
set p = ConceptStr(# O,A #);
for x being object st x in O holds
x in (AttributeDerivation C) . A9

proof

let x9 be object ; :: thesis: ( x9 in O implies x9 in (AttributeDerivation C) . A9 )
assume A27: x9 in O ; :: thesis: x9 in (AttributeDerivation C) . A9
then reconsider x9 = x9 as Object of C ;
for a being Attribute of C st a in A9 holds
x9 is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in A9 implies x9 is-connected-with a )
assume a in A9 ; :: thesis: x9 is-connected-with a
then consider x being Element of X such that
A28: a in the Intent of x by A18;
x9 in (AttributeDerivation C) . the Intent of x by A19, A27;
then x9 in { o where o is Object of C : for a being Attribute of C st a in the Intent of x holds
o is-connected-with a } by Def3;
then ex y being Object of C st
( y = x9 & ( for a being Attribute of C st a in the Intent of x holds
y is-connected-with a ) ) ;
hence x9 is-connected-with a by A28; :: thesis: verum

end;

then x9 in { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ;
hence x9 in (AttributeDerivation C) . A9 by Def3; :: thesis: verum

end;

then O = (AttributeDerivation C) . A9 by A23, TARSKI:2;
then ConceptStr(# O,A #) is FormalConcept of C by A26, Th21;
then reconsider p = ConceptStr(# O,A #) as Element of (ConceptLattice C) by Th31;
A29: for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= p

proof

let b be Element of (ConceptLattice C); :: thesis: ( b is_less_than X implies b [= p )
assume A30: b is_less_than X ; :: thesis: b [= p
the Extent of (b @) c= the Extent of (p @)

proof

let x9 be object ; :: according to TARSKI:def 3 :: thesis: ( not x9 in the Extent of (b @) or x9 in the Extent of (p @) )
assume A31: x9 in the Extent of (b @) ; :: thesis: x9 in the Extent of (p @)
then reconsider x9 = x9 as Object of C ;
for x being Element of X holds x9 in the Extent of x

proof

let x be Element of X; :: thesis: x9 in the Extent of x
x in X ;
then reconsider x = x as Element of (ConceptLattice C) ;
b [= x by A30, LATTICE3:def 16;
then b @ is-SubConcept-of x @ by Th43;
then the Extent of (b @) c= the Extent of (x @) ;
hence x9 in the Extent of x by A31; :: thesis: verum

end;

hence x9 in the Extent of (p @) by A9; :: thesis: verum

end;

then b @ is-SubConcept-of p @ ;
hence b [= p by Th43; :: thesis: verum

end;

for q being Element of (ConceptLattice C) st q in X holds
p [= q

proof

let q be Element of (ConceptLattice C); :: thesis: ( q in X implies p [= q )
assume A32: q in X ; :: thesis: p [= q
the Extent of (p @) c= the Extent of (q @) by A9, A32;
then p @ is-SubConcept-of q @ ;
hence p [= q by Th43; :: thesis: verum

end;

then p is_less_than X by LATTICE3:def 16;
hence ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) ) by A29; :: thesis: verum

end;

end;

end;

hence ConceptLattice C is complete Lattice by VECTSP_8:def 6; :: thesis: verum