let C be strict FormalContext; :: thesis: for CP being strict FormalConcept of C holds (CP .: ) .: = CP
let CP be strict FormalConcept of C; :: thesis: (CP .: ) .: = CP
A1: the Extent of ((CP .: ) .: ) = the Intent of (CP .: ) by Def8
.= the Extent of CP by Def8 ;
the Intent of ((CP .: ) .: ) = the Extent of (CP .: ) by Def8
.= the Intent of CP by Def8 ;
hence (CP .: ) .: = CP by A1; :: thesis: verum