let C be FormalContext; :: thesis: for CP1, CP2 being FormalConcept of C holds
( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 )
let CP1, CP2 be FormalConcept of C; :: thesis: ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 )
A1: now :: thesis: ( the Intent of CP2 c= the Intent of CP1 implies CP1 is-SubConcept-of CP2 )
assume the Intent of CP2 c= the Intent of CP1 ; :: thesis: CP1 is-SubConcept-of CP2
then A2: (AttributeDerivation C) . the Intent of CP1 c= (AttributeDerivation C) . the Intent of CP2 by Th4;
( (AttributeDerivation C) . the Intent of CP1 = the Extent of CP1 & (AttributeDerivation C) . the Intent of CP2 = the Extent of CP2 ) by Def9;
hence CP1 is-SubConcept-of CP2 by A2; :: thesis: verum
end;
now :: thesis: ( CP1 is-SubConcept-of CP2 implies the Intent of CP2 c= the Intent of CP1 )
assume CP1 is-SubConcept-of CP2 ; :: thesis: the Intent of CP2 c= the Intent of CP1
then A3: the Extent of CP1 c= the Extent of CP2 ;
( (ObjectDerivation C) . the Extent of CP2 = the Intent of CP2 & (ObjectDerivation C) . the Extent of CP1 = the Intent of CP1 ) by Def9;
hence the Intent of CP2 c= the Intent of CP1 by A3, Th3; :: thesis: verum
end;
hence ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 ) by A1; :: thesis: verum