let C be 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 )
let o be Object of C; 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; ( 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 ( (gamma C) . o [= (delta C) . a implies o is-connected-with a )
assume
o is-connected-with a
;
(gamma C) . o [= (delta C) . athen
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;
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
; 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
; verum