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 [:O,A:] c= the Information of C )
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 [:O,A:] c= the Information of C )
let A be Subset of the carrier' of C; :: thesis: ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C )
A1: ( [:O,A:] c= the Information of C implies O c= (AttributeDerivation C) . A )

proof

assume A2: [:O,A:] c= the Information of C ; :: thesis: O c= (AttributeDerivation C) . A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in O or x in (AttributeDerivation C) . A )
assume A3: x in O ; :: thesis: x in (AttributeDerivation C) . A
then reconsider x = x as Object of C ;
for a being Attribute of C st a in A holds
x is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in A implies x is-connected-with a )
consider z being set such that
A4: z = [x,a] ;
assume a in A ; :: thesis: x is-connected-with a
then z in [:O,A:] by A3, A4, ZFMISC_1:def 2;
hence x is-connected-with a by A2, A4; :: thesis: verum

end;

then x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ;
hence x in (AttributeDerivation C) . A by Def3; :: thesis: verum

end;

( O c= (AttributeDerivation C) . A implies [:O,A:] c= the Information of C )

proof

assume O c= (AttributeDerivation C) . A ; :: thesis: [:O,A:] c= the Information of C
then A5: O c= { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } by Def3;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:O,A:] or z in the Information of C )
assume z in [:O,A:] ; :: thesis: z in the Information of C
then consider x, y being object such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Attribute of C by A7;
reconsider x = x as Object of C by A6;
x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } by A5, A6;
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A holds
x9 is-connected-with a ) ) ;
then x is-connected-with y by A7;
hence z in the Information of C by A8; :: thesis: verum

end;

hence ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) by A1; :: thesis: verum