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: { 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
A2: ( q = ConceptStr(# O,A #) & 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
A3: ( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) by A2;
A4: {o} c= the Extent of CP by A3, ZFMISC_1:37;
A5: (ObjectDerivation C) . the Extent of CP = the Intent of CP by CONLAT_1:def 13;
the Intent of (q @ ) = (ObjectDerivation C) . {o} by A2, A3, CONLAT_1:def 24;
then the Intent of CP c= the Intent of (q @ ) by A4, A5, CONLAT_1:3;
then A6: q @ is-SubConcept-of CP by CONLAT_1:31;
CP = (@ CP) @ by CONLAT_1:def 24;
hence q [= @ CP by A6, CONLAT_1:47; :: thesis: verum

end;

for CP' 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 CP' holds
@ CP [= CP'

proof

let CP' 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 CP' implies @ CP [= CP' )
assume A7: { 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' ; :: thesis: @ CP [= CP'
A8: the Extent of CP c= the Extent of (CP' @ )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Extent of CP or x in the Extent of (CP' @ ) )
assume A9: x in the Extent of CP ; :: thesis: x in the Extent of (CP' @ )
then reconsider x = x as Element of the carrier of C ;
set Ox = (AttributeDerivation C) . ((ObjectDerivation C) . {x});
set Ax = (ObjectDerivation C) . {x};
reconsider Cx = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . {x})),((ObjectDerivation C) . {x}) #) as strict FormalConcept of C by CONLAT_1:20;
{x} c= (AttributeDerivation C) . ((ObjectDerivation C) . {x}) by CONLAT_1:5;
then A10: x in the Extent 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 o being Object of C st
( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } by A9;
then @ Cx [= CP' by A7, LATTICE3:def 17;
then A11: (@ Cx) @ is-SubConcept-of CP' @ by CONLAT_1:47;
Cx = (@ Cx) @ by CONLAT_1:def 24;
then the Extent of Cx c= the Extent of (CP' @ ) by A11, CONLAT_1:def 19;
hence x in the Extent of (CP' @ ) by A10; :: thesis: verum

end;

CP = (@ CP) @ by CONLAT_1:def 24;
then (@ CP) @ is-SubConcept-of CP' @ by A8, CONLAT_1:def 19;
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 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