let C be FormalContext; :: thesis: for CP being strict FormalConcept of C holds "/\" { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C) = CP
let CP be strict FormalConcept of C; :: thesis: "/\" { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C) = CP
set D = { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ;
A1: @ CP is_less_than { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) }

proof

let q be Element of (ConceptLattice C); :: according to LATTICE3:def 16 :: thesis: ( not q in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } or @ CP [= q )
assume q in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ; :: thesis: @ CP [= q
then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A2: ( q = ConceptStr(# O,A #) & ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) ;
consider a being Attribute of C such that
A3: ( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) by A2;
A4: {a} c= the Intent of CP by A3, ZFMISC_1:37;
A5: (AttributeDerivation C) . the Intent of CP = the Extent of CP by CONLAT_1:def 13;
the Extent of (q @ ) = (AttributeDerivation C) . {a} by A2, A3, CONLAT_1:def 24;
then the Extent of CP c= the Extent of (q @ ) by A4, A5, CONLAT_1:4;
then A6: CP is-SubConcept-of q @ by CONLAT_1:def 19;
CP = (@ CP) @ by CONLAT_1:def 24;
hence @ CP [= q by A6, CONLAT_1:47; :: thesis: verum

end;

for CP' being Element of (ConceptLattice C) st CP' is_less_than { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } holds
CP' [= @ CP

proof

let CP' be Element of (ConceptLattice C); :: thesis: ( CP' is_less_than { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } implies CP' [= @ CP )
assume A7: CP' is_less_than { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ; :: thesis: CP' [= @ CP
A8: the Intent of CP c= the Intent of (CP' @ )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Intent of CP or x in the Intent of (CP' @ ) )
assume A9: x in the Intent of CP ; :: thesis: x in the Intent of (CP' @ )
then reconsider x = x as Element of the carrier' of C ;
set Ox = (AttributeDerivation C) . {x};
set Ax = (ObjectDerivation C) . ((AttributeDerivation C) . {x});
reconsider Cx = ConceptStr(# ((AttributeDerivation C) . {x}),((ObjectDerivation C) . ((AttributeDerivation C) . {x})) #) as strict FormalConcept of C by CONLAT_1:22;
{x} c= (ObjectDerivation C) . ((AttributeDerivation C) . {x}) by CONLAT_1:6;
then A10: x in the Intent of Cx by ZFMISC_1:37;
Cx in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } by A9;
then CP' [= @ Cx by A7, LATTICE3:def 16;
then A11: CP' @ is-SubConcept-of (@ Cx) @ by CONLAT_1:47;
Cx = (@ Cx) @ by CONLAT_1:def 24;
then the Intent of Cx c= the Intent of (CP' @ ) by A11, CONLAT_1:31;
hence x in the Intent of (CP' @ ) by A10; :: thesis: verum

end;

CP = (@ CP) @ by CONLAT_1:def 24;
then CP' @ is-SubConcept-of (@ CP) @ by A8, CONLAT_1:31;
hence CP' [= @ CP by CONLAT_1:47; :: thesis: verum

end;

hence "/\" { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C) = CP by A1, LATTICE3:34; :: thesis: verum