let C be FormalContext; :: thesis: for D being non empty Subset of (ConceptLattice C) holds
( 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 } )
let D be non empty Subset of (ConceptLattice C); :: thesis: ( 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 } )
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 } ));
set A9 = (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 } );
set y = the Element of 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 } c= bool the carrier of C

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

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

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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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 } or x in the carrier of C )
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: x in the carrier of C
then consider Y being set such that
A1: x in Y and
A2: 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;
ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( Y = the Extent 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 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 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 } )) or x in the carrier of C )
A3: (AttributeDerivation C) . ((ObjectDerivation C) . u) is Element of bool the carrier of C ;
assume 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: x in the carrier of C
hence x in the carrier of C by A3; :: thesis: verum

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 ;
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 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 reconsider OO = OO as non empty Subset-Family of the carrier of C ;
A6: { 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) . O9) where O9 is Subset of the carrier of C : O9 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 } }

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 { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 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 { 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 { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 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 E being Subset of the carrier of C, I being Subset of the carrier' of C such that
A7: x = the Intent of ConceptStr(# E,I #) and
A8: ConceptStr(# E,I #) in D ;
ConceptStr(# E,I #) is FormalConcept of C by A5, A8;
then A9: x = (ObjectDerivation C) . the Extent of ConceptStr(# E,I #) by A7, CONLAT_1:def 10;
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 A8;
hence x in { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 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 A9; :: thesis: verum

end;

{ ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 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 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 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 { 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 { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 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 { 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 O9 being Subset of the carrier of C such that
A10: x = (ObjectDerivation C) . O9 and
A11: O9 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
A12: O9 = the Extent 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 Intent of ConceptStr(# E,I #) by A10, A12, CONLAT_1:def 10;
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 A13; :: thesis: verum

end;

then A14: { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 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 } by A6;
A15: (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) . O9) where O9 is Subset of the carrier of C : O9 in OO } by Th2;
(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

set y = the Element of D;
set Y = the 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 } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 } ) 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 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 the 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 } 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 A17: ex E1 being Subset of the carrier of C ex I1 being Subset of the carrier' of C st
( the 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 } = the Intent of ConceptStr(# E1,I1 #) & ConceptStr(# E1,I1 #) in D ) ;
assume 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: x in the carrier' of C
then x in the 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 } by A15, A14, A16, SETFAM_1:def 1;
hence x in the carrier' of C by A17; :: thesis: verum

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 ;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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 } or x in the carrier of C )
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: x in the carrier of C
then consider Y being set such that
A18: x in Y and
A19: 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;
ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( Y = the Extent 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:19;
reconsider CP = CP9 as Element of (ConceptLattice C) by A4, CONLAT_1:31;
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 A15, A14, CONLAT_1:def 21;
A21: 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: ( D is_less_than r implies CP [= r )
assume A22: D is_less_than r ; :: thesis: CP [= r
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: ( q in D implies the Intent of (r @) c= the Intent of (q @) )
assume q in D ; :: thesis: the Intent of (r @) c= the Intent of (q @)
then q [= r by A22;
then q @ is-SubConcept-of r @ by CONLAT_1:43;
hence the Intent of (r @) c= the Intent of (q @) by CONLAT_1:28; :: thesis: verum

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

set y = the Element of D;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Intent of (r @) or 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 } )
assume A24: x in the Intent of (r @) ; :: thesis: 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 }
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: ( 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 } implies x in Y )
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: 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 Intent of ConceptStr(# Ey,Iy #) and
A27: 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 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 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 } ;
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 A25, SETFAM_1:def 1; :: thesis: verum

end;

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

end;

D is_less_than CP

proof

let q be Element of (ConceptLattice C); :: according to LATTICE3:def 17 :: thesis: ( not q in D or q [= CP )
assume q in D ; :: thesis: q [= CP
then q @ in D by CONLAT_1:def 21;
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:3;
then q @ is-SubConcept-of CP @ by CONLAT_1:28;
hence q [= CP by CONLAT_1:43; :: thesis: verum

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 A15, A14, A21, LATTICE3:def 21; :: thesis: verum