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

assume CP1 [= CP2 ; :: thesis: CP1 @ is-SubConcept-of CP2 @
then CP1 "\/" CP2 = CP2 by LATTICES:def 3;
then A2: the L_join of (ConceptLattice C) . CP1,CP2 = CP2 by LATTICES:def 1;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A3: ( (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 Def22;
for x being set st x in the Intent of (CP2 @ ) holds
x in the Intent of (CP1 @ ) by A2, A3, XBOOLE_0:def 4;
then the Intent of (CP2 @ ) c= the Intent of (CP1 @ ) by TARSKI:def 3;
hence CP1 @ is-SubConcept-of CP2 @ by Th31; :: thesis: verum

end;

now

assume A4: CP1 @ is-SubConcept-of CP2 @ ; :: thesis: CP1 [= CP2
then the Intent of (CP2 @ ) c= the Intent of (CP1 @ ) by Th31;
then A5: the Intent of (CP1 @ ) /\ the Intent of (CP2 @ ) = the Intent of (CP2 @ ) by XBOOLE_1:28;
the Extent of (CP1 @ ) c= the Extent of (CP2 @ ) by A4, Def19;
then A6: the Extent of (CP1 @ ) \/ the Extent of (CP2 @ ) = the Extent of (CP2 @ ) by XBOOLE_1:12;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A7: ( (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 Def22;
O = (AttributeDerivation C) . the Intent of (CP2 @ ) by A6, A7, Def13
.= the Extent of (CP2 @ ) by Def13 ;
then CP1 "\/" CP2 = CP2 by A5, A7, LATTICES:def 1;
hence CP1 [= CP2 by LATTICES:def 3; :: thesis: verum

end;

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