let C be FormalContext; 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; "\/" ( { 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
{ 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);
LATTICE3:def 17 ( 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} ) }
;
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;
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; verum