theorem :: CONLAT_1:1

for C being FormalContext
for o being Object of C holds (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a }