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 )
set aa = {a};
set o9 = {o};
set oo = (AttributeDerivation C) . ((ObjectDerivation C) . {o});
consider O being Subset of the carrier of C, A being Subset of the carrier' of C 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 { a9 where a9 is Attribute of C : o is-connected-with a9 } ;
then a in (ObjectDerivation C) . {o} by CONLAT_1:1;
then A3: {a} c= (ObjectDerivation C) . {o} by ZFMISC_1:31;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C 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 O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A6: (delta C) . a = ConceptStr(# O9,A9 #) and
A7: O9 = (AttributeDerivation C) . {a} and
A9 = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) by Def5;
A8: the Extent of (((delta C) . a) @) = O9 by A6, CONLAT_1:def 21;
the Extent of (((gamma C) . o) @) = O by A4, CONLAT_1:def 21;
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 16;
hence (gamma C) . o [= (delta C) . a by CONLAT_1:43; :: thesis: verum

end;

consider O9 being Subset of the carrier of C, A9 being Subset of the carrier' of C such that
A9: (delta C) . a = ConceptStr(# O9,A9 #) and
A10: O9 = (AttributeDerivation C) . {a} and
A9 = (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:43;
then A11: the Extent of (((gamma C) . o) @) c= the Extent of (((delta C) . a) @) by CONLAT_1:def 16;
the Extent of (((delta C) . a) @) = O9 by A9, CONLAT_1:def 21;
then O c= O9 by A11, A1, CONLAT_1:def 21;
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:31;
then a in { a9 where a9 is Attribute of C : o is-connected-with a9 } by CONLAT_1:1;
then ex b being Attribute of C st
( b = a & o is-connected-with b ) ;
hence o is-connected-with a ; :: thesis: verum