let C be FormalContext; :: thesis: for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (ObjectDerivation (C .:)) . A
let O be Subset of the carrier' of C; :: thesis: (AttributeDerivation C) . O = (ObjectDerivation (C .:)) . O
reconsider O9 = O as Subset of the carrier of (C .:) ;
set A1 = { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } ;
set A2 = { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } ;
A1: { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } c= { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a }
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } or u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } )
assume u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } ; :: thesis: u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a }
then consider a being Object of C such that
A2: a = u and
A3: for o being Attribute of C st o in O holds
a is-connected-with o ;
reconsider u9 = u as Attribute of (C .:) by A2;
for o being Object of (C .:) st o in O9 holds
o is-connected-with u9
proof
let o9 be Object of (C .:); :: thesis: ( o9 in O9 implies o9 is-connected-with u9 )
reconsider o = o9 as Attribute of C ;
assume o9 in O9 ; :: thesis: o9 is-connected-with u9
then a is-connected-with o by A3;
then [a,o] in the Information of C by CONLAT_1:def 2;
then [o9,u9] in the Information of (C .:) by A2, RELAT_1:def 7;
hence o9 is-connected-with u9 by CONLAT_1:def 2; :: thesis: verum
end;
hence u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } ; :: thesis: verum
end;
A4: { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } c= { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o }
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } or u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } )
assume u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } ; :: thesis: u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o }
then consider a being Attribute of (C .:) such that
A5: a = u and
A6: for o being Object of (C .:) st o in O9 holds
o is-connected-with a ;
reconsider u9 = u as Object of C by A5;
for o being Attribute of C st o in O holds
u9 is-connected-with o
proof
let o9 be Attribute of C; :: thesis: ( o9 in O implies u9 is-connected-with o9 )
reconsider o = o9 as Object of (C .:) ;
assume o9 in O ; :: thesis: u9 is-connected-with o9
then o is-connected-with a by A6;
then [o,a] in the Information of (C .:) by CONLAT_1:def 2;
then [u9,o9] in the Information of C by A5, RELAT_1:def 7;
hence u9 is-connected-with o9 by CONLAT_1:def 2; :: thesis: verum
end;
hence u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } ; :: thesis: verum
end;
( (AttributeDerivation C) . O = { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } & (ObjectDerivation (C .:)) . O9 = { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } ) by CONLAT_1:def 3, CONLAT_1:def 4;
hence (AttributeDerivation C) . O = (ObjectDerivation (C .:)) . O by A1, A4; :: thesis: verum