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 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 for q being Element of (ConceptLattice C) st q in X holds
Top (ConceptLattice C) [= q ;
then A1: Top (ConceptLattice C) is_less_than X by LATTICE3:def 16;
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 Th35;
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 Th35;
reconsider CO = CO as strict FormalConcept of C ;
(B-join C) . CO,CP = (B-join C) . CP,CO by Th37
.= CO by Th43 ;
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) by LATTICES:def 17;
hence b [= Top (ConceptLattice C) by LATTICES:def 3; :: thesis: verum

end;

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 A1; :: 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 } ;
A2: 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;
A3: meet ExX c= the carrier of C

proof

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

end;

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 )
A6: ( 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 A2;
hence o in the Extent of x by A7, SETFAM_1:def 1; :: thesis: verum

end;

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

proof

assume A8: 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 Y' being Element of B-carrier C st
( Y = the Extent of Y' & Y' in X ) ;
hence o in Y by A8; :: thesis: verum

end;

hence o in meet ExX by 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 A6; :: 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 A3;
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: 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 set ; :: 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
A11: ( x in Y & Y in { the Intent of x where x is Element of B-carrier C : x in X } ) by TARSKI:def 4;
consider Y' being Element of B-carrier C such that
A12: ( Y = the Intent of Y' & Y' in X ) by A11;
thus x in the carrier' of C by A11, A12; :: thesis: verum

end;

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 )
A13: ( 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 & Y in { the Intent of x where x is Element of B-carrier C : x in X } ) by TARSKI:def 4;
consider Y' being Element of B-carrier C such that
A15: ( Y = the Intent of Y' & Y' in X ) by A14;
thus ex x being Element of X st a in the Intent of x by A14, A15; :: thesis: verum

end;

( 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 A16: 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
A17: a in the Intent of x by A16;
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 A17; :: 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;

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 A13; :: thesis: verum

end;

then consider A' being Subset of the carrier' of C such that
A18: for a being Attribute of C holds
( a in A' iff ex x being Element of X st a in the Intent of x ) by A10;
consider A being Subset of the carrier' of C such that
A19: A = (ObjectDerivation C) . ((AttributeDerivation C) . A') ;
set p = ConceptStr(# O,A #);
ConceptStr(# O,A #) is FormalConcept of C

proof

O = (AttributeDerivation C) . A'

proof

A20: 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 )
A21: ( 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 Def13; :: thesis: verum

end;

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

end;

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

proof

assume A23: 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 A23;
hence o in the Extent of x by Def13; :: thesis: verum

end;

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

end;

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

end;

A24: for x being set st x in O holds
x in (AttributeDerivation C) . A'

proof

let x' be set ; :: thesis: ( x' in O implies x' in (AttributeDerivation C) . A' )
assume A25: x' in O ; :: thesis: x' in (AttributeDerivation C) . A'
then reconsider x' = x' as Object of C ;
for a being Attribute of C st a in A' holds
x' is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in A' implies x' is-connected-with a )
assume a in A' ; :: thesis: x' is-connected-with a
then consider x being Element of X such that
A26: a in the Intent of x by A18;
x' in (AttributeDerivation C) . the Intent of x by A20, A25;
then x' 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 Def7;
then consider y being Object of C such that
A27: ( y = x' & ( for a being Attribute of C st a in the Intent of x holds
y is-connected-with a ) ) ;
thus x' is-connected-with a by A26, A27; :: thesis: verum

end;

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

end;

for x being set st x in (AttributeDerivation C) . A' holds
x in O

proof

let x be set ; :: thesis: ( x in (AttributeDerivation C) . A' implies x in O )
assume x in (AttributeDerivation C) . A' ; :: thesis: x in O
then x in { o where o is Object of C : for a being Attribute of C st a in A' holds
o is-connected-with a } by Def7;
then consider x' being Object of C such that
A28: ( x' = x & ( for a being Attribute of C st a in A' holds
x' is-connected-with a ) ) ;
for x being Element of X holds x' in (AttributeDerivation C) . the Intent of x

proof

let x be Element of X; :: thesis: x' in (AttributeDerivation C) . the Intent of x
for a being Attribute of C st a in the Intent of x holds
x' is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in the Intent of x implies x' is-connected-with a )
assume a in the Intent of x ; :: thesis: x' is-connected-with a
then a in A' by A18;
hence x' is-connected-with a by A28; :: thesis: verum

end;

then x' 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 x' in (AttributeDerivation C) . the Intent of x by Def7; :: thesis: verum

end;

hence x in O by A20, A28; :: thesis: verum

end;

hence O = (AttributeDerivation C) . A' by A24, TARSKI:2; :: thesis: verum

end;

hence ConceptStr(# O,A #) is FormalConcept of C by A19, Th22; :: thesis: verum

end;

then reconsider p = ConceptStr(# O,A #) as Element of (ConceptLattice C) by Th35;
A29: p is_less_than X

proof

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 A30: q in X ; :: thesis: p [= q
the Extent of (p @ ) c= the Extent of (q @ )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Extent of (p @ ) or x in the Extent of (q @ ) )
assume x in the Extent of (p @ ) ; :: thesis: x in the Extent of (q @ )
hence x in the Extent of (q @ ) by A9, A30; :: thesis: verum

end;

then p @ is-SubConcept-of q @ by Def19;
hence p [= q by Th47; :: thesis: verum

end;

hence p is_less_than X by LATTICE3:def 16; :: thesis: verum

end;

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 A31: b is_less_than X ; :: thesis: b [= p
the Extent of (b @ ) c= the Extent of (p @ )

proof

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

proof

let x be Element of X; :: thesis: x' in the Extent of x
x in X ;
then reconsider x = x as Element of (ConceptLattice C) ;
b [= x by A31, LATTICE3:def 16;
then b @ is-SubConcept-of x @ by Th47;
then A33: the Extent of (b @ ) c= the Extent of (x @ ) by Def19;
thus x' in the Extent of x by A32, A33; :: thesis: verum

end;

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

end;

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

end;

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