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 o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ,(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 o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ,(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 o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ;
A1: for CP9 being Element of (ConceptLattice C) st { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } is_less_than CP9 holds
@ CP [= CP9
proof
let CP9 be Element of (ConceptLattice C); :: thesis: ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } is_less_than CP9 implies @ CP [= CP9 )
assume A2: { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } is_less_than CP9 ; :: thesis: @ CP [= CP9
A3: the Extent of CP c= the Extent of (CP9 @)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Extent of CP or x in the Extent of (CP9 @) )
assume A4: x in the Extent of CP ; :: thesis: x in the Extent of (CP9 @)
then reconsider x = x as Element of C ;
set Ax = (ObjectDerivation C) . {x};
set Ox = (AttributeDerivation C) . ((ObjectDerivation C) . {x});
reconsider Cx = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . {x})),((ObjectDerivation C) . {x}) #) as strict FormalConcept of C by CONLAT_1:19;
Cx in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } by A4;
then @ Cx [= CP9 by A2;
then A5: (@ Cx) @ is-SubConcept-of CP9 @ by CONLAT_1:43;
{x} c= (AttributeDerivation C) . ((ObjectDerivation C) . {x}) by CONLAT_1:5;
then A6: x in the Extent of Cx by ZFMISC_1:31;
Cx = (@ Cx) @ by CONLAT_1:def 21;
then the Extent of Cx c= the Extent of (CP9 @) by A5, CONLAT_1:def 16;
hence x in the Extent of (CP9 @) by A6; :: thesis: verum
end;
CP = (@ CP) @ by CONLAT_1:def 21;
then (@ CP) @ is-SubConcept-of CP9 @ by A3, CONLAT_1:def 16;
hence @ CP [= CP9 by CONLAT_1:43; :: thesis: verum
end;
{ ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } is_less_than @ CP
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def 17 :: 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 o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } or q [= @ CP )
assume q in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ; :: thesis: q [= @ CP
then consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A7: q = ConceptStr(# O,A #) and
A8: ex o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ;
consider o being Object of C such that
A9: o in the Extent of CP and
O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) and
A10: A = (ObjectDerivation C) . {o} by A8;
A11: {o} c= the Extent of CP by A9, ZFMISC_1:31;
( (ObjectDerivation C) . the Extent of CP = the Intent of CP & the Intent of (q @) = (ObjectDerivation C) . {o} ) by A7, A10, CONLAT_1:def 10, CONLAT_1:def 21;
then the Intent of CP c= the Intent of (q @) by A11, CONLAT_1:3;
then A12: q @ is-SubConcept-of CP by CONLAT_1:28;
CP = (@ CP) @ by CONLAT_1:def 21;
hence q [= @ CP by A12, CONLAT_1:43; :: 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 o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ,(ConceptLattice C)) = CP by A1, LATTICE3:def 21; :: thesis: verum