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 Intent of ((CP .:) .:) = the Extent of (CP .:) by Def8
.= the Intent of CP by Def8 ;
the Extent of ((CP .:) .:) = the Intent of (CP .:) by Def8
.= the Extent of CP by Def8 ;
hence (CP .:) .: = CP by A1; :: thesis: verum