let C be FormalContext; :: thesis: for O being Subset of
for A being Subset of holds
( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
let O be Subset of ; :: thesis: for A being Subset of holds
( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
let A be Subset of ; :: 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