let C be FormalContext; :: thesis: for D being non empty Subset of (ConceptLattice C) holds
( the Extent of ("/\" (D,C)) = meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } & the Intent of ("/\" (D,C)) = (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) )
let D be non empty Subset of (ConceptLattice C); :: thesis: ( the Extent of ("/\" (D,C)) = meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } & the Intent of ("/\" (D,C)) = (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) )
set A = (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ));
set O9 = (AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } );
set y = the Element of D;
{ the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } c= bool the carrier' of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } or x in bool the carrier' of C )
assume x in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ; :: thesis: x in bool the carrier' of C
then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( x = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ;
hence x in bool the carrier' of C ; :: thesis: verum

end;

then reconsider AA = { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } as Subset-Family of the carrier' of C ;
(ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) c= the carrier' of C

proof

set u = union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ;
union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } c= the carrier' of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } or x in the carrier' of C )
assume x in union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ; :: thesis: x in the carrier' of C
then consider Y being set such that
A1: x in Y and
A2: Y in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } by TARSKI:def 4;
ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( Y = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A2;
hence x in the carrier' of C by A1; :: thesis: verum

end;

then reconsider u = union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } as Subset of the carrier' of C ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) or x in the carrier' of C )
A3: (ObjectDerivation C) . ((AttributeDerivation C) . u) is Element of bool the carrier' of C ;
assume x in (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) ; :: thesis: x in the carrier' of C
hence x in the carrier' of C by A3; :: thesis: verum

end;

then reconsider a = (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) as Subset of the carrier' of C ;
A4: ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 20;
A5: for x being object st x in D holds
( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) )

proof

let x be object ; :: thesis: ( x in D implies ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) )
assume x in D ; :: thesis: ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) )
then x is strict FormalConcept of C by A4, CONLAT_1:31;
hence ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) ; :: thesis: verum

end;

then ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) ;
then the Intent of the Element of D in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ;
then reconsider AA = AA as non empty Subset-Family of the carrier' of C ;
A6: { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } c= { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } or x in { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } } )
assume x in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ; :: thesis: x in { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } }
then consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that
A7: x = the Extent of ConceptStr(# E,I #) and
A8: ConceptStr(# E,I #) in D ;
ConceptStr(# E,I #) is FormalConcept of C by A5, A8;
then A9: x = (AttributeDerivation C) . the Intent of ConceptStr(# E,I #) by A7, CONLAT_1:def 10;
the Intent of ConceptStr(# E,I #) in { the Intent of ConceptStr(# EE,II #) where EE is Subset of the carrier of C, II is Subset of the carrier' of C : ConceptStr(# EE,II #) in D } by A8;
hence x in { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } } by A9; :: thesis: verum

end;

{ ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } } c= { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } } or x in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )
assume x in { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } } ; :: thesis: x in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D }
then consider A9 being Subset of the carrier' of C such that
A10: x = (AttributeDerivation C) . A9 and
A11: A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ;
consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that
A12: A9 = the Intent of ConceptStr(# E,I #) and
A13: ConceptStr(# E,I #) in D by A11;
ConceptStr(# E,I #) is FormalConcept of C by A5, A13;
then x = the Extent of ConceptStr(# E,I #) by A10, A12, CONLAT_1:def 10;
hence x in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } by A13; :: thesis: verum

end;

then A14: { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } } = { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } by A6;
A15: (AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ) = meet { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in AA } by Th3;
(AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ) c= the carrier of C

proof

set y = the Element of D;
set Y = the Element of { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ) or x in the carrier of C )
ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5;
then A16: the Extent of the Element of D in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ;
then the Element of { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ;
then A17: ex E1 being Subset of the carrier of C ex I1 being Subset of the carrier' of C st
( the Element of { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } = the Extent of ConceptStr(# E1,I1 #) & ConceptStr(# E1,I1 #) in D ) ;
assume x in (AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ) ; :: thesis: x in the carrier of C
then x in the Element of { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } by A15, A14, A16, SETFAM_1:def 1;
hence x in the carrier of C by A17; :: thesis: verum

end;

then reconsider o = (AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ) as Subset of the carrier of C ;
union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } c= the carrier' of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } or x in the carrier' of C )
assume x in union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ; :: thesis: x in the carrier' of C
then consider Y being set such that
A18: x in Y and
A19: Y in { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } by TARSKI:def 4;
ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( Y = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A19;
hence x in the carrier' of C by A18; :: thesis: verum

end;

then reconsider CP9 = ConceptStr(# o,a #) as strict FormalConcept of C by CONLAT_1:21;
reconsider CP = CP9 as Element of (ConceptLattice C) by A4, CONLAT_1:31;
A20: the Extent of (CP @) = meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } by A15, A14, CONLAT_1:def 21;
A21: for r being Element of (ConceptLattice C) st r is_less_than D holds
r [= CP

proof

let r be Element of (ConceptLattice C); :: thesis: ( r is_less_than D implies r [= CP )
assume A22: r is_less_than D ; :: thesis: r [= CP
A23: for q being Element of (ConceptLattice C) st q in D holds
the Extent of (r @) c= the Extent of (q @)

proof

let q be Element of (ConceptLattice C); :: thesis: ( q in D implies the Extent of (r @) c= the Extent of (q @) )
assume q in D ; :: thesis: the Extent of (r @) c= the Extent of (q @)
then r [= q by A22;
then r @ is-SubConcept-of q @ by CONLAT_1:43;
hence the Extent of (r @) c= the Extent of (q @) by CONLAT_1:def 16; :: thesis: verum

end;

the Extent of (r @) c= meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D }

proof

set y = the Element of D;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Extent of (r @) or x in meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )
assume A24: x in the Extent of (r @) ; :: thesis: x in meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D }
A25: for Y being set st Y in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } holds
x in Y

proof

let Y be set ; :: thesis: ( Y in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } implies x in Y )
assume Y in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ; :: thesis: x in Y
then consider Ey being Subset of the carrier of C, Iy being Subset of the carrier' of C such that
A26: Y = the Extent of ConceptStr(# Ey,Iy #) and
A27: ConceptStr(# Ey,Iy #) in D ;
reconsider C1 = ConceptStr(# Ey,Iy #) as Element of (ConceptLattice C) by A27;
the Extent of (r @) c= the Extent of (C1 @) by A23, A27;
then x in the Extent of (C1 @) by A24;
hence x in Y by A26, CONLAT_1:def 21; :: thesis: verum

end;

ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5;
then the Extent of the Element of D in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ;
hence x in meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } by A25, SETFAM_1:def 1; :: thesis: verum

end;

then r @ is-SubConcept-of CP @ by A20, CONLAT_1:def 16;
hence r [= CP by CONLAT_1:43; :: thesis: verum

end;

CP is_less_than D

proof

let q be Element of (ConceptLattice C); :: according to LATTICE3:def 16 :: thesis: ( not q in D or CP [= q )
assume q in D ; :: thesis: CP [= q
then q @ in D by CONLAT_1:def 21;
then the Extent of (q @) in { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } ;
then the Extent of (CP @) c= the Extent of (q @) by A20, SETFAM_1:3;
then CP @ is-SubConcept-of q @ by CONLAT_1:def 16;
hence CP [= q by CONLAT_1:43; :: thesis: verum

end;

hence ( the Extent of ("/\" (D,C)) = meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } & the Intent of ("/\" (D,C)) = (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) ) by A15, A14, A21, LATTICE3:34; :: thesis: verum