let C be FormalContext; :: thesis: for CP being strict FormalConcept of strict holds "/\" { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of 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 strict ; :: thesis: "/\" { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of 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 , A is Subset of : ex a being Attribute of st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ;
A1: for CP' being Element of st CP' is_less_than { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of 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 ; :: thesis: ( CP' is_less_than { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } implies CP' [= @ CP )
assume A2: CP' is_less_than { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ; :: thesis: CP' [= @ CP
A3: 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 A4: 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 Ax = (ObjectDerivation C) . ((AttributeDerivation C) . {x});
set Ox = (AttributeDerivation C) . {x};
reconsider Cx = ConceptStr(# ((AttributeDerivation C) . {x}),((ObjectDerivation C) . ((AttributeDerivation C) . {x})) #) as strict FormalConcept of strict by CONLAT_1:22;
Cx in { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } by A4;
then CP' [= @ Cx by A2, LATTICE3:def 16;
then A5: CP' @ is-SubConcept-of (@ Cx) @ by CONLAT_1:47;
{x} c= (ObjectDerivation C) . ((AttributeDerivation C) . {x}) by CONLAT_1:6;
then A6: x in the Intent of Cx by ZFMISC_1:37;
Cx = (@ Cx) @ by CONLAT_1:def 24;
then the Intent of Cx c= the Intent of (CP' @ ) by A5, CONLAT_1:31;
hence x in the Intent of (CP' @ ) by A6; :: thesis: verum

end;

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

end;

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

proof

let q be Element of ; :: according to LATTICE3:def 16 :: thesis: ( not q in { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of 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 , A is Subset of : ex a being Attribute of 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 , A being Subset of such that
A7: q = ConceptStr(# O,A #) and
A8: ex a being Attribute of st
( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ;
consider a being Attribute of such that
A9: a in the Intent of CP and
A10: O = (AttributeDerivation C) . {a} and
A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) by A8;
A11: {a} c= the Intent of CP by A9, ZFMISC_1:37;
( (AttributeDerivation C) . the Intent of CP = the Extent of CP & the Extent of (q @ ) = (AttributeDerivation C) . {a} ) by A7, A10, CONLAT_1:def 13, CONLAT_1:def 24;
then the Extent of CP c= the Extent of (q @ ) by A11, CONLAT_1:4;
then A12: CP is-SubConcept-of q @ by CONLAT_1:def 19;
CP = (@ CP) @ by CONLAT_1:def 24;
hence @ CP [= q by A12, CONLAT_1:47; :: thesis: verum

end;

hence "/\" { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of 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