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