let C be FormalContext; :: thesis: for O being Subset of holds O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)
let O be Subset of ; :: thesis: O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)
set A = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
for x being set st 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 } holds
x in the carrier' of C

proof

let x be set ; :: thesis: ( 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 } implies x in the carrier' of C )
assume 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 } ; :: thesis: x in the carrier' of C
then ex x' being Attribute of C st
( x' = x & ( for o being Object of C st o in O holds
o is-connected-with x' ) ) ;
hence x in the carrier' of C ; :: thesis: verum

end;

then reconsider A = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } as Subset of by TARSKI:def 3;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in O or x in (AttributeDerivation C) . ((ObjectDerivation C) . O) )
assume A1: x in O ; :: thesis: x in (AttributeDerivation C) . ((ObjectDerivation C) . O)
then reconsider x = x as Object of C ;
A2: 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 )
assume a in A ; :: thesis: x is-connected-with a
then ex a' being Attribute of C st
( a' = a & ( for o being Object of C st o in O holds
o is-connected-with a' ) ) ;
hence x is-connected-with a by A1; :: thesis: verum

end;

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