let C be FormalContext; :: thesis: (ObjectDerivation C) . {} = the carrier' of C
reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2;
A1: (ObjectDerivation C) . e = { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } by Def6;
set A = { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } ;
A2: for x being set st x in { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } holds
x in the carrier' of C

proof

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

proof

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

end;

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