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: ( [:O,A:] c= the Information of C implies A c= (ObjectDerivation C) . O )
proof
assume A2: [:O,A:] c= the Information of C ; :: thesis: A c= (ObjectDerivation C) . O
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (ObjectDerivation C) . O )
assume A3: 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 )
consider z being set such that
A4: z = [o,x] ;
assume o in O ; :: thesis: o is-connected-with x
then z in [:O,A:] by A3, A4, ZFMISC_1:def 2;
hence o is-connected-with x by A2, A4; :: 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 Def2; :: thesis: verum
end;
( 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 A5: 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 Def2;
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;
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 A5, A7;
then ex y9 being Attribute of C st
( y9 = y & ( for o being Object of C st o in O holds
o is-connected-with y9 ) ) ;
then x is-connected-with y by A6;
hence z in the Information of C by A8; :: thesis: verum
end;
hence ( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C ) by A1; :: thesis: verum