let C be FormalContext; :: thesis: for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O))
let O be Subset of the carrier of C; :: thesis: (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O))
set A = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
set O9 = { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ;
set A9 = { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ;
A1: for x being object st x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } holds
x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }

proof

let x be object ; :: thesis: ( x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } implies x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } )
assume x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
then A2: ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with x9 ) ) ;
then reconsider x = x as Attribute of C ;
for o being Object of C st o in O holds
o is-connected-with x

proof

let o be Object of C; :: thesis: ( o in O implies o is-connected-with x )
assume A3: o in O ; :: thesis: o is-connected-with x

now :: thesis: ( ( o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } & o is-connected-with x ) or ( not o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } & o is-connected-with x ) )

per cases ( o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } or not o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ) ;

case o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: o is-connected-with x

hence o is-connected-with x by A2; :: thesis: verum

end;

case not o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: o is-connected-with x

then consider a being Attribute of C such that
A4: a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } and
A5: not o is-connected-with a ;
ex a9 being Attribute of C st
( a9 = a & ( for o being Object of C st o in O holds
o is-connected-with a9 ) ) by A4;
hence o is-connected-with x by A3, A5; :: thesis: verum

end;

end;

end;

hence o is-connected-with x ; :: thesis: verum

end;

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

end;

for x being object st x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a }

proof

let x be object ; :: thesis: ( x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } implies x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } )
assume A6: x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; :: thesis: x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a }
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O holds
o is-connected-with x9 ) ) ;
then reconsider x = x as Attribute of C ;
for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with x

proof

let o be Object of C; :: thesis: ( o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } implies o is-connected-with x )
assume o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: o is-connected-with x
then ex o9 being Object of C st
( o9 = o & ( for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o9 is-connected-with a ) ) ;
hence o is-connected-with x by A6; :: thesis: verum

end;

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

end;

then A7: { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } = { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } by A1, TARSKI:2;
{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } c= the carrier' of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } or x in the carrier' of C )
assume x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; :: thesis: x in the carrier' of C
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O holds
o is-connected-with x9 ) ) ;
hence x in the carrier' of C ; :: thesis: verum

end;

then reconsider A = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } as Subset of the carrier' of C ;
{ o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } c= the carrier of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } or x in the carrier of C )
assume x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: x in the carrier of C
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A holds
x9 is-connected-with a ) ) ;
hence x in the carrier of C ; :: thesis: verum

end;

then reconsider O9 = { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } as Subset of the carrier of C ;
( A = (ObjectDerivation C) . O & O9 = (AttributeDerivation C) . A ) by Def2, Def3;
hence (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O)) by A7, Def2; :: thesis: verum