theorem Th13: :: CONLAT_2:13

for C being FormalContext
for o being Object of C
for a being Attribute of C holds
( o is-connected-with a iff (gamma C) . o [= (delta C) . a )