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

proof

assume A c= (ObjectDerivation C) . O ; :: thesis: [:O,A:] c= the Information of C
then A2: A c= { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } by Def6;
let z be set ; :: 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 set such that
A3: ( x in O & y in A & z = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x as Object of C by A3;
reconsider y = y as Attribute of C by A3;
y in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } by A2, A3;
then consider y' being Attribute of C such that
A4: ( y' = y & ( for o being Object of C st o in O holds
o is-connected-with y' ) ) ;
x is-connected-with y by A3, A4;
hence z in the Information of C by A3, Def5; :: thesis: verum

end;

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

proof

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

proof

let o be Object of C; :: thesis: ( o in O implies o is-connected-with x )
assume A7: o in O ; :: thesis: o is-connected-with x
consider z being set such that
A8: z = [o,x] ;
z in [:O,A:] by A6, A7, A8, ZFMISC_1:def 2;
hence o is-connected-with x by A5, A8, Def5; :: thesis: verum

end;

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

end;

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