let C be FormalContext; :: thesis: (AttributeDerivation C) . {} = the carrier of C
reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
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 } ;
A1: for x being object 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 object ; :: 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 ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in e holds
x9 is-connected-with a ) ) ;
hence x in the carrier of C ; :: thesis: verum
end;
A2: for x being object 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 object ; :: 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;
(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 Def3;
hence (AttributeDerivation C) . {} = the carrier of C by A1, A2, TARSKI:2; :: thesis: verum