let C be FormalContext; :: thesis:
let D be non empty Subset of (ConceptLattice C); :: thesis:
set O = (AttributeDerivation C) . ((ObjectDerivation C) . (union { 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 } ));
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 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= bool the carrier of C

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
A3: ( x = the Extent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ;
thus x in bool the carrier of C by A3; :: thesis:

end;

then reconsider OO = { 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 } as Subset-Family of the carrier of C ;
set A' = (ObjectDerivation C) . (union { 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
A4: y = ConceptStr(# E',I' #) by A2;
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 A4;
then reconsider OO = OO as non empty Subset-Family of the carrier of C ;
A5: (ObjectDerivation C) . (union { 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 } ) = meet { ((ObjectDerivation C) . O') where O' is Subset of the carrier of C : O' in OO } by Th2;
A6: { ((ObjectDerivation C) . O') where O' is Subset of the carrier of C : O' 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 } } = { 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

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

proof

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

end;

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

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
A9: ( x = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ;
ConceptStr(# E,I #) is FormalConcept of C by A2, A9;
then A10: x = (ObjectDerivation C) . the Extent of ConceptStr(# E,I #) by A9, CONLAT_1:def 13;
the Extent of ConceptStr(# E,I #) in { the Extent 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 { ((ObjectDerivation C) . O') where O' is Subset of the carrier of C : O' 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 A10; :: thesis:

end;

(ObjectDerivation C) . (union { 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= the carrier' of C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in (ObjectDerivation C) . (union { 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:
consider Y being Element of { 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
A12: y = ConceptStr(# E',I' #) by A2;
A13: 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 A12;
then 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 } ;
then consider E1 being Subset of the carrier of C, I1 being Subset of the carrier' of C such that
A14: ( Y = the Intent 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 a = (ObjectDerivation C) . (union { 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 } ) as Subset of the carrier' of C ;
(AttributeDerivation C) . ((ObjectDerivation C) . (union { 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= the carrier of C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: x in (AttributeDerivation C) . ((ObjectDerivation C) . (union { 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:
set u = union { 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 } ;
union { 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= the carrier of C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union { 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 Y being set such that
A16: ( x in Y & 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 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 Extent 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 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 } as Subset of the carrier of C ;
(AttributeDerivation C) . ((ObjectDerivation C) . u) is Element of bool the carrier of C ;
hence x in the carrier of C by A15; :: thesis:

end;

then reconsider o = (AttributeDerivation C) . ((ObjectDerivation C) . (union { 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 } )) as Subset of the carrier of C ;
union { 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= the carrier of C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union { 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 Y being set such that
A18: ( x in Y & 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 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 Extent 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:20;
reconsider CP = CP' as Element of (ConceptLattice C) by A1, CONLAT_1:35;
A20: the Intent of (CP @ ) = meet { 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, CONLAT_1:def 24;
A21: D is_less_than CP

proof

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

end;

for r being Element of (ConceptLattice C) st D is_less_than r holds
CP [= r

proof

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

proof

let q be Element of (ConceptLattice C); :: thesis:
assume q in D ; :: thesis:
then q [= r by A22, LATTICE3:def 17;
then q @ is-SubConcept-of r @ by CONLAT_1:47;
hence the Intent of (r @ ) c= the Intent of (q @ ) by CONLAT_1:31; :: thesis:

end;

the Intent of (r @ ) c= meet { 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 set ; :: according to TARSKI:def 3 :: thesis:
assume A24: x in the Intent 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 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 A25;
for Y being set st 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 } holds
x in Y

proof

let Y be set ; :: thesis:
assume 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 } ; :: thesis:
then consider Ey being Subset of the carrier of C, Iy being Subset of the carrier' of C such that
A27: ( Y = the Intent of ConceptStr(# Ey,Iy #) & ConceptStr(# Ey,Iy #) in D ) ;
reconsider C1 = ConceptStr(# Ey,Iy #) as Element of (ConceptLattice C) by A27;
the Intent of (r @ ) c= the Intent of (C1 @ ) by A23, A27;
then x in the Intent of (C1 @ ) by A24;
hence x in Y by A27, CONLAT_1:def 24; :: thesis:

end;

hence x in meet { 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 A26, SETFAM_1:def 1; :: thesis:

end;

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

end;

hence ( the Extent of ("\/" D,C) = (AttributeDerivation C) . ((ObjectDerivation C) . (union { 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) = meet { 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:def 21; :: thesis: