let C be FormalContext; :: thesis: for O being Subset of holds (ObjectDerivation C) . O = (AttributeDerivation (C .: )) . O
let O be Subset of ; :: thesis: (ObjectDerivation C) . O = (AttributeDerivation (C .: )) . O
reconsider O' = O as Subset of ;
set A1 = { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a } ;
set A2 = { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o } ;
A1: { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a } c= { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a } or u in { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o } )
assume u in { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a } ; :: thesis: u in { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o }
then consider a being Attribute of such that
A2: a = u and
A3: for o being Object of st o in O holds
o is-connected-with a ;
reconsider u' = u as Object of by A2;
for o' being Attribute of st o' in O' holds
u' is-connected-with o'

proof

let o' be Attribute of ; :: thesis: ( o' in O' implies u' is-connected-with o' )
reconsider o = o' as Object of ;
assume o' in O' ; :: thesis: u' is-connected-with o'
then o is-connected-with a by A3;
then [o,a] in the Information of C by CONLAT_1:def 5;
then [a,o] in the Information of (C .: ) by RELAT_1:def 7;
hence u' is-connected-with o' by A2, CONLAT_1:def 5; :: thesis: verum

end;

hence u in { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o } ; :: thesis: verum

end;

A4: { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o } c= { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o } or u in { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a } )
assume u in { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o } ; :: thesis: u in { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a }
then consider a being Object of such that
A5: a = u and
A6: for o being Attribute of st o in O' holds
a is-connected-with o ;
reconsider u' = u as Attribute of by A5;
for o being Object of st o in O holds
o is-connected-with u'

proof

let o' be Object of ; :: thesis: ( o' in O implies o' is-connected-with u' )
reconsider o = o' as Attribute of ;
assume o' in O ; :: thesis: o' is-connected-with u'
then a is-connected-with o by A6;
then [a,o] in the Information of (C .: ) by CONLAT_1:def 5;
then [o',u'] in the Information of C by A5, RELAT_1:def 7;
hence o' is-connected-with u' by CONLAT_1:def 5; :: thesis: verum

end;

hence u in { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a } ; :: thesis: verum

end;

( (ObjectDerivation C) . O = { a where a is Attribute of : for o being Object of st o in O holds
o is-connected-with a } & (AttributeDerivation (C .: )) . O' = { a where a is Object of : for o being Attribute of st o in O' holds
a is-connected-with o } ) by CONLAT_1:def 6, CONLAT_1:def 7;
hence (ObjectDerivation C) . O = (AttributeDerivation (C .: )) . O by A1, A4, XBOOLE_0:def 10; :: thesis: verum