let C be FormalContext; :: thesis: for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
let O be Subset of the carrier of C; :: thesis: for A being Subset of the carrier' of C holds
( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
let A be Subset of the carrier' of C; :: thesis: ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) by Th9;
hence ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O ) by Th10; :: thesis: verum