let C be FormalContext; :: thesis: for a being Attribute of C holds (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a }
let a be Attribute of C; :: thesis: (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a }
{a} c= the carrier' of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a} or x in the carrier' of C )
assume x in {a} ; :: thesis: x in the carrier' of C
then x = a by TARSKI:def 1;
hence x in the carrier' of C ; :: thesis: verum

end;

then reconsider t = {a} as Subset of the carrier' of C ;
A1: for x being object st x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } holds
x in { o where o is Object of C : o is-connected-with a }

proof

set a9 = the Element of t;
let x be object ; :: thesis: ( x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } implies x in { o where o is Object of C : o is-connected-with a } )
reconsider a9 = the Element of t as Attribute of C by TARSKI:def 1;
A2: a9 = a by TARSKI:def 1;
assume x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } ; :: thesis: x in { o where o is Object of C : o is-connected-with a }
then A3: ex x9 being Object of C st
( x9 = x & ( for a9 being Attribute of C st a9 in t holds
x9 is-connected-with a9 ) ) ;
then reconsider x = x as Object of C ;
x is-connected-with a9 by A3;
hence x in { o where o is Object of C : o is-connected-with a } by A2; :: thesis: verum

end;

A4: for x being object st x in { o where o is Object of C : o is-connected-with a } holds
x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 }

proof

let x be object ; :: thesis: ( x in { o where o is Object of C : o is-connected-with a } implies x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } )
assume x in { o where o is Object of C : o is-connected-with a } ; :: thesis: x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 }
then A5: ex x9 being Object of C st
( x9 = x & x9 is-connected-with a ) ;
then reconsider x = x as Object of C ;
for a9 being Attribute of C st a9 in t holds
x is-connected-with a9 by A5, TARSKI:def 1;
hence x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } ; :: thesis: verum

end;

(AttributeDerivation C) . t = { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } by Def3;
hence (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a } by A1, A4, TARSKI:2; :: thesis: verum