let C be FormalContext; :: thesis: for O being Subset of the carrier of C holds O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)
let O be Subset of the carrier of C; :: 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 object 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 object ; :: 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 x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O holds
o is-connected-with x9 ) ) ;
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 the carrier' of C by TARSKI:def 3;
let x be object ; :: 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 a9 being Attribute of C st
( a9 = a & ( for o being Object of C st o in O holds
o is-connected-with a9 ) ) ;
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 Def3;
then x in (AttributeDerivation C) . A by A2;
hence x in (AttributeDerivation C) . ((ObjectDerivation C) . O) by Def2; :: thesis: verum