let C be FormalContext; :: thesis: for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A))
let A be Subset of the carrier' of C; :: thesis: (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A))
set O = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ;
set 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 holds
o is-connected-with a } holds
o is-connected-with a } ;
set O' = { 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ;
A1: for x being set st x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a }

proof

let x be set ; :: thesis: ( x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } implies 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } )
assume A2: x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; :: thesis: 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a }
then consider x' being Object of C such that
A3: ( x' = x & ( for a being Attribute of C st a in A holds
x' is-connected-with a ) ) ;
reconsider x = x as Object of C by A3;
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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
x is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a 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 holds
o is-connected-with a } holds
o is-connected-with a } implies x is-connected-with a )
assume a 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 holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: x is-connected-with a
then consider a' being Attribute of C such that
A4: ( a' = a & ( 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 holds
o is-connected-with a } holds
o is-connected-with a' ) ) ;
thus x is-connected-with a by A2, A4; :: thesis: verum

end;

hence 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: verum

end;

for x being set st 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } holds
x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }

proof

let x be set ; :: thesis: ( 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } implies x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } )
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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
then consider x' being Object of C such that
A5: ( x' = x & ( 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
x' is-connected-with a ) ) ;
reconsider x = x as Object of C by A5;
for a being Attribute of C st a in A holds
x is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in A implies x is-connected-with a )
assume A6: a in A ; :: thesis: x is-connected-with a

now

per cases ( a 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 holds
o is-connected-with a } holds
o is-connected-with a } or not a 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 holds
o is-connected-with a } holds
o is-connected-with a } ) ;

case a 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 holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: x is-connected-with a

hence x is-connected-with a by A5; :: thesis: verum

end;

case not a 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 holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: x is-connected-with a

then consider o being Object of C such that
A7: ( o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } & not o is-connected-with a ) ;
consider o' being Object of C such that
A8: ( o' = o & ( for a being Attribute of C st a in A holds
o' is-connected-with a ) ) by A7;
thus x is-connected-with a by A6, A7, A8; :: thesis: verum

end;

end;

end;

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

end;

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

end;

then A9: { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } = { 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } by A1, TARSKI:2;
{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } c= the carrier of C

proof

let x be set ; :: 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 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 holds
o is-connected-with a } ; :: thesis: x in the carrier of C
then consider x' being Object of C such that
A10: ( x' = x & ( for a being Attribute of C st a in A holds
x' is-connected-with a ) ) ;
thus x in the carrier of C by A10; :: thesis: verum

end;

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

proof

let x be set ; :: 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } 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 where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } ; :: thesis: x in the carrier' of C
then consider x' being Attribute of C such that
A11: ( x' = x & ( for o being Object of C st o in O holds
o is-connected-with x' ) ) ;
thus x in the carrier' of C by A11; :: thesis: verum

end;

then reconsider 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 holds
o is-connected-with a } holds
o is-connected-with a } as Subset of the carrier' of C ;
A12: O = (AttributeDerivation C) . A by Def7;
A' = (ObjectDerivation C) . O by Def6;
hence (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A)) by A9, A12, Def7; :: thesis: verum