let C be FormalContext; :: thesis:
let D be non empty Subset of (ConceptLattice C); :: thesis:
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 } ));
A1: ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def 23;
A2: for x being set 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 set ; :: thesis:
assume x in D ; :: thesis:
then x is strict FormalConcept of C by A1, CONLAT_1:35;
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:

end;

{ 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 set ; :: according to TARSKI:def 3 :: thesis:
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:
then consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that
A3: ( x = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ;
thus x in bool the carrier' of C by A3; :: thesis:

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 ;
set 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 } );
consider y being Element of D;
consider E' being Subset of the carrier of C, I' being Subset of the carrier' of C such that
A4: y = ConceptStr(# E',I' #) by A2;
the Intent of 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 A4;
then reconsider AA = AA as non empty Subset-Family of the carrier' of C ;
A5: (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) . A') where A' is Subset of the carrier' of C : A' in AA } by Th3;
A6: { ((AttributeDerivation C) . A') where A' is Subset of the carrier' of C : A' 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 }

proof

thus { ((AttributeDerivation C) . A') where A' is Subset of the carrier' of C : A' 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 } :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { ((AttributeDerivation C) . A') where A' is Subset of the carrier' of C : A' 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:
then consider A' being Subset of the carrier' of C such that
A7: ( x = (AttributeDerivation C) . A' & A' 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
A8: ( A' = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A7;
ConceptStr(# E,I #) is FormalConcept of C by A2, A8;
then x = the Extent of ConceptStr(# E,I #) by A7, A8, CONLAT_1:def 13;
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 A8; :: thesis:

end;

thus { 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) . A') where A' is Subset of the carrier' of C : A' 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:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
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:
then consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that
A9: ( x = the Extent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ;
ConceptStr(# E,I #) is FormalConcept of C by A2, A9;
then A10: x = (AttributeDerivation C) . the Intent of ConceptStr(# E,I #) by A9, CONLAT_1:def 13;
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 A9;
hence x in { ((AttributeDerivation C) . A') where A' is Subset of the carrier' of C : A' 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 A10; :: thesis:

end;

(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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: 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:
consider Y being 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 } ;
consider y being Element of D;
consider E' being Subset of the carrier of C, I' being Subset of the carrier' of C such that
A12: y = ConceptStr(# E',I' #) by A2;
A13: the Extent of 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 } by A12;
then 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 } ;
then consider E1 being Subset of the carrier of C, I1 being Subset of the carrier' of C such that
A14: ( Y = the Extent of ConceptStr(# E1,I1 #) & ConceptStr(# E1,I1 #) in D ) ;
x in Y by A5, A6, A11, A13, SETFAM_1:def 1;
hence x in the carrier of C by A14; :: thesis:

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 ;
(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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: 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:
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 set ; :: according to TARSKI:def 3 :: thesis:
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:
then consider Y being set such that
A16: ( x in Y & 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;
consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that
A17: ( Y = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A16;
thus x in the carrier' of C by A16, A17; :: thesis:

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 ;
(ObjectDerivation C) . ((AttributeDerivation C) . u) is Element of bool the carrier' of C ;
hence x in the carrier' of C by A15; :: thesis:

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 ;
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 set ; :: according to TARSKI:def 3 :: thesis:
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:
then consider Y being set such that
A18: ( x in Y & 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;
consider E being Subset of the carrier of C, I being Subset of the carrier' of C such that
A19: ( Y = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A18;
thus x in the carrier' of C by A18, A19; :: thesis:

end;

then reconsider CP' = ConceptStr(# o,a #) as strict FormalConcept of C by CONLAT_1:22;
reconsider CP = CP' as Element of (ConceptLattice C) by A1, CONLAT_1:35;
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 A5, A6, CONLAT_1:def 24;
A21: CP is_less_than D

proof

let q be Element of (ConceptLattice C); :: according to LATTICE3:def 16 :: thesis:
assume q in D ; :: thesis:
then q @ in D by CONLAT_1:def 24;
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:4;
then CP @ is-SubConcept-of q @ by CONLAT_1:def 19;
hence CP [= q by CONLAT_1:47; :: thesis:

end;

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:
assume A22: r is_less_than D ; :: thesis:
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:
assume q in D ; :: thesis:
then r [= q by A22, LATTICE3:def 16;
then r @ is-SubConcept-of q @ by CONLAT_1:47;
hence the Extent of (r @ ) c= the Extent of (q @ ) by CONLAT_1:def 19; :: thesis:

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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A24: x in the Extent of (r @ ) ; :: thesis:
consider y being Element of D;
consider E' being Subset of the carrier of C, I' being Subset of the carrier' of C such that
A25: y = ConceptStr(# E',I' #) by A2;
A26: the Extent of 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 } by 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:
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:
then consider Ey being Subset of the carrier of C, Iy being Subset of the carrier' of C such that
A27: ( Y = the Extent of ConceptStr(# Ey,Iy #) & 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 A27, CONLAT_1:def 24; :: thesis:

end;

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 A26, SETFAM_1:def 1; :: thesis:

end;

then r @ is-SubConcept-of CP @ by A20, CONLAT_1:def 19;
hence r [= CP by CONLAT_1:47; :: thesis:

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 A5, A6, A21, LATTICE3:34; :: thesis: