let C be FormalContext; :: thesis: (AttributeDerivation C) . {} = the carrier of C
reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
A1: (AttributeDerivation C) . e = { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } by Def7;
set O = { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } ;
A2: for x being set st x in { o where o is Object of C : for a being Attribute of C st a in e 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 e 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 e holds
o is-connected-with a } ; :: thesis: x in the carrier of C
then consider x' being Object of C such that
A3: ( x' = x & ( for a being Attribute of C st a in e holds
x' is-connected-with a ) ) ;
thus x in the carrier of C by A3; :: thesis: verum

end;

for x being set st x in the carrier of C holds
x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a }

proof

let x be set ; :: thesis: ( x in the carrier of C implies x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } )
assume x in the carrier of C ; :: thesis: x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a }
then reconsider x = x as Object of C ;
for a being Attribute of C st a in e holds
x is-connected-with a ;
hence x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } ; :: thesis: verum

end;

hence (AttributeDerivation C) . {} = the carrier of C by A1, A2, TARSKI:2; :: thesis: verum