let C be FormalContext; :: thesis: for o being Object of
for a being Attribute of holds
( o is-connected-with a iff (gamma C) . o [= (delta C) . a )
let o be Object of ; :: thesis: for a being Attribute of holds
( o is-connected-with a iff (gamma C) . o [= (delta C) . a )
let a be Attribute of ; :: thesis: ( o is-connected-with a iff (gamma C) . o [= (delta C) . a )
set aa = {a};
set o' = {o};
set oo = (AttributeDerivation C) . ((ObjectDerivation C) . {o});
consider O being Subset of , A being Subset of such that
A1: (gamma C) . o = ConceptStr(# O,A #) and
A2: O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) and
A = (ObjectDerivation C) . {o} by Def4;

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 : o is-connected-with a' } ;
then a in (ObjectDerivation C) . {o} by CONLAT_1:1;
then A3: {a} c= (ObjectDerivation C) . {o} by ZFMISC_1:37;
consider O being Subset of , A being Subset of such that
A4: (gamma C) . o = ConceptStr(# O,A #) and
A5: O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) and
A = (ObjectDerivation C) . {o} by Def4;
consider O' being Subset of , A' being Subset of such that
A6: (delta C) . a = ConceptStr(# O',A' #) and
A7: O' = (AttributeDerivation C) . {a} and
A' = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) by Def5;
A8: the Extent of (((delta C) . a) @ ) = O' by A6, CONLAT_1:def 24;
the Extent of (((gamma C) . o) @ ) = O by A4, CONLAT_1:def 24;
then the Extent of (((gamma C) . o) @ ) c= the Extent of (((delta C) . a) @ ) by A3, A5, A7, A8, 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;

consider O' being Subset of , A' being Subset of such that
A9: (delta C) . a = ConceptStr(# O',A' #) and
A10: O' = (AttributeDerivation C) . {a} and
A' = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) by Def5;
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 A11: the Extent of (((gamma C) . o) @ ) c= the Extent of (((delta C) . a) @ ) by CONLAT_1:def 19;
the Extent of (((delta C) . a) @ ) = O' by A9, CONLAT_1:def 24;
then O c= O' by A11, A1, CONLAT_1:def 24;
then {a} c= (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . {o})) by A2, A10, 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 : o is-connected-with a' } by CONLAT_1:1;
then ex b being Attribute of st
( b = a & o is-connected-with b ) ;
hence o is-connected-with a ; :: thesis: verum