let C be FormalContext; :: thesis: 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 )
let o be Object of C; :: thesis: for a being Attribute of C holds
( o is-connected-with a iff (gamma C) . o [= (delta C) . a )
let a be Attribute of C; :: thesis: ( o is-connected-with a iff (gamma C) . o [= (delta C) . a )

hereby :: thesis: ( (gamma C) . o [= (delta C) . a implies o is-connected-with a )

assume o is-connected-with a ; :: thesis: (gamma C) . o [= (delta C) . a
then a in { a' where a' is Attribute of C : o is-connected-with a' } ;
then a in (ObjectDerivation C) . {o} by CONLAT_1:1;
then A1: {a} c= (ObjectDerivation C) . {o} by ZFMISC_1:37;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A2: ( (gamma C) . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) by Def4;
consider O' being Subset of the carrier of C, A' being Subset of the carrier' of C such that
A3: ( (delta C) . a = ConceptStr(# O',A' #) & O' = (AttributeDerivation C) . {a} & A' = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) by Def5;
A4: the Extent of (((gamma C) . o) @ ) = O by A2, CONLAT_1:def 24;
the Extent of (((delta C) . a) @ ) = O' by A3, CONLAT_1:def 24;
then the Extent of (((gamma C) . o) @ ) c= the Extent of (((delta C) . a) @ ) by A1, A2, A3, A4, CONLAT_1:4;
then ((gamma C) . o) @ is-SubConcept-of ((delta C) . a) @ by CONLAT_1:def 19;
hence (gamma C) . o [= (delta C) . a by CONLAT_1:47; :: thesis: verum

end;

assume (gamma C) . o [= (delta C) . a ; :: thesis: o is-connected-with a
then ((gamma C) . o) @ is-SubConcept-of ((delta C) . a) @ by CONLAT_1:47;
then A5: the Extent of (((gamma C) . o) @ ) c= the Extent of (((delta C) . a) @ ) by CONLAT_1:def 19;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A6: ( (gamma C) . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) by Def4;
consider O' being Subset of the carrier of C, A' being Subset of the carrier' of C such that
A7: ( (delta C) . a = ConceptStr(# O',A' #) & O' = (AttributeDerivation C) . {a} & A' = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) by Def5;
the Extent of (((delta C) . a) @ ) = O' by A7, CONLAT_1:def 24;
then A8: O c= O' by A5, A6, CONLAT_1:def 24;
set aa = {a};
set o' = {o};
set oo = (AttributeDerivation C) . ((ObjectDerivation C) . {o});
{a} c= (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . {o})) by A6, A7, A8, CONLAT_1:11;
then {a} c= (ObjectDerivation C) . {o} by CONLAT_1:7;
then a in (ObjectDerivation C) . {o} by ZFMISC_1:37;
then a in { a' where a' is Attribute of C : o is-connected-with a' } by CONLAT_1:1;
then consider b being Attribute of C such that
A9: ( b = a & o is-connected-with b ) ;
thus o is-connected-with a by A9; :: thesis: verum