let C be FormalContext; :: thesis: for O1, O2 being Subset of the carrier of C st O1 c= O2 holds
(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1
let O1, O2 be Subset of the carrier of C; :: thesis: ( O1 c= O2 implies (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1 )
assume A1: O1 c= O2 ; :: thesis: (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (ObjectDerivation C) . O2 or x in (ObjectDerivation C) . O1 )
assume x in (ObjectDerivation C) . O2 ; :: thesis: x in (ObjectDerivation C) . O1
then x in { a where a is Attribute of C : for o being Object of C st o in O2 holds
o is-connected-with a } by Def2;
then consider x9 being Attribute of C such that
A2: x9 = x and
A3: for o being Object of C st o in O2 holds
o is-connected-with x9 ;
for o being Object of C st o in O1 holds
o is-connected-with x9 by A1, A3;
then x in { a where a is Attribute of C : for o being Object of C st o in O1 holds
o is-connected-with a } by A2;
hence x in (ObjectDerivation C) . O1 by Def2; :: thesis: verum