let C be FormalContext; :: thesis: for A being Subset of the carrier' of C holds A c= (ObjectDerivation C) . ((AttributeDerivation C) . A)
let A be Subset of the carrier' of C; :: thesis: A c= (ObjectDerivation C) . ((AttributeDerivation C) . A)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (ObjectDerivation C) . ((AttributeDerivation C) . A) )
assume A1: x in A ; :: thesis: x in (ObjectDerivation C) . ((AttributeDerivation C) . A)
then reconsider x = x as Attribute of C ;
set O = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ;
{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } c= the carrier of C

proof

for x being set st 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 } holds
x in the carrier of C

proof

let x be set ; :: thesis: ( 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 } implies x in the carrier of C )
assume 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 } ; :: thesis: x in the carrier of C
then consider x' being Object of C such that
A2: ( x' = x & ( for a being Attribute of C st a in A holds
x' is-connected-with a ) ) ;
thus x in the carrier of C by A2; :: thesis: verum

end;

hence { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } c= the carrier of C by TARSKI:def 3; :: thesis: verum

end;

then reconsider O = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } as Subset of the carrier of C ;
A3: 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 o in O ; :: thesis: o is-connected-with x
then consider o' being Object of C such that
A4: ( o' = o & ( for a being Attribute of C st a in A holds
o' is-connected-with a ) ) ;
thus o is-connected-with x by A1, A4; :: thesis: verum

end;

(ObjectDerivation C) . O = { 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;
then x in (ObjectDerivation C) . O by A3;
hence x in (ObjectDerivation C) . ((AttributeDerivation C) . A) by Def7; :: thesis: verum