let C be FormalContext; :: thesis: for CP1, CP2 being Element of (ConceptLattice C) holds
( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )
let CP1, CP2 be Element of (ConceptLattice C); :: thesis: ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )
set CL = ConceptLattice C;

A1: now :: thesis: ( CP1 @ is-SubConcept-of CP2 @ implies CP1 [= CP2 )

assume A2: CP1 @ is-SubConcept-of CP2 @ ; :: thesis: CP1 [= CP2
then the Intent of (CP2 @) c= the Intent of (CP1 @) by Th28;
then A3: the Intent of (CP1 @) /\ the Intent of (CP2 @) = the Intent of (CP2 @) by XBOOLE_1:28;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A4: (B-join C) . ((CP1 @),(CP2 @)) = ConceptStr(# O,A #) and
A5: O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of (CP1 @) \/ the Extent of (CP2 @))) and
A6: A = the Intent of (CP1 @) /\ the Intent of (CP2 @) by Def18;
the Extent of (CP1 @) c= the Extent of (CP2 @) by A2;
then the Extent of (CP1 @) \/ the Extent of (CP2 @) = the Extent of (CP2 @) by XBOOLE_1:12;
then O = (AttributeDerivation C) . the Intent of (CP2 @) by A5, Def9
.= the Extent of (CP2 @) by Def9 ;
then CP1 "\/" CP2 = CP2 by A3, A4, A6, LATTICES:def 1;
hence CP1 [= CP2 by LATTICES:def 3; :: thesis: verum

end;

now :: thesis: ( CP1 [= CP2 implies CP1 @ is-SubConcept-of CP2 @ )

assume CP1 [= CP2 ; :: thesis: CP1 @ is-SubConcept-of CP2 @
then CP1 "\/" CP2 = CP2 by LATTICES:def 3;
then A7: the L_join of (ConceptLattice C) . (CP1,CP2) = CP2 by LATTICES:def 1;
ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-join C) . ((CP1 @),(CP2 @)) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of (CP1 @) \/ the Extent of (CP2 @))) & A = the Intent of (CP1 @) /\ the Intent of (CP2 @) ) by Def18;
then for x being object st x in the Intent of (CP2 @) holds
x in the Intent of (CP1 @) by A7, XBOOLE_0:def 4;
then the Intent of (CP2 @) c= the Intent of (CP1 @) ;
hence CP1 @ is-SubConcept-of CP2 @ by Th28; :: thesis: verum

end;

hence ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ ) by A1; :: thesis: verum