let C be FormalContext; :: thesis: for D being non empty Subset-Family of the carrier' of C holds (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }
let D be non empty Subset-Family of the carrier' of C; :: thesis: (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }
reconsider D' = D as non empty Subset-Family of the carrier' of C ;
set OU = (AttributeDerivation C) . (union D);
set M = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ;

now

per cases ( { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } <> {} or { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = {} ) ;

case A1: { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } <> {} ; :: thesis: (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }

thus (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } :: thesis: verum

proof

thus (AttributeDerivation C) . (union D) c= meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } :: according to XBOOLE_0:def 10 :: thesis: meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } c= (AttributeDerivation C) . (union D)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (AttributeDerivation C) . (union D) or x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } )
assume x in (AttributeDerivation C) . (union D) ; :: thesis: x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }
then x in { o' where o' is Object of C : for a being Attribute of C st a in union D' holds
o' is-connected-with a } by CONLAT_1:def 7;
then consider x' being Object of C such that
A2: ( x' = x & ( for a being Attribute of C st a in union D holds
x' is-connected-with a ) ) ;
reconsider x = x as Object of C by A2;
A3: for A being Subset of the carrier' of C st A in D holds
for a being Attribute of C st a in A holds
x is-connected-with a

proof

let A be Subset of the carrier' of C; :: thesis: ( A in D implies for a being Attribute of C st a in A holds
x is-connected-with a )
assume A4: A in D ; :: thesis: for a being Attribute of C st a in A holds
x is-connected-with a
let a be Attribute of C; :: thesis: ( a in A implies x is-connected-with a )
assume a in A ; :: thesis: x is-connected-with a
then a in union D by A4, TARSKI:def 4;
hence x is-connected-with a by A2; :: thesis: verum

end;

A5: for A being Subset of the carrier' of C st A in D holds
x in (AttributeDerivation C) . A

proof

let A be Subset of the carrier' of C; :: thesis: ( A in D implies x in (AttributeDerivation C) . A )
assume A in D ; :: thesis: x in (AttributeDerivation C) . A
then for a being Attribute of C st a in A holds
x is-connected-with a by A3;
then 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 } ;
hence x in (AttributeDerivation C) . A by CONLAT_1:def 7; :: thesis: verum

end;

for Y being set st Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } holds
x in Y

proof

let Y be set ; :: thesis: ( Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } implies x in Y )
assume Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; :: thesis: x in Y
then consider A being Subset of the carrier' of C such that
A6: ( Y = (AttributeDerivation C) . A & A in D ) ;
thus x in Y by A5, A6; :: thesis: verum

end;

hence x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } by A1, SETFAM_1:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } or x in (AttributeDerivation C) . (union D) )
assume A7: x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; :: thesis: x in (AttributeDerivation C) . (union D)
consider d being Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ;
A8: d in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } by A1;
A9: x in d by A1, A7, SETFAM_1:def 1;
consider X being Subset of the carrier' of C such that
A10: ( d = (AttributeDerivation C) . X & X in D ) by A8;
reconsider x = x as Object of C by A9, A10;
A11: for A being Subset of the carrier' of C st A in D holds
x in (AttributeDerivation C) . A

proof

let A be Subset of the carrier' of C; :: thesis: ( A in D implies x in (AttributeDerivation C) . A )
assume A in D ; :: thesis: x in (AttributeDerivation C) . A
then (AttributeDerivation C) . A in { ((AttributeDerivation C) . A') where A' is Subset of the carrier' of C : A' in D } ;
hence x in (AttributeDerivation C) . A by A7, SETFAM_1:def 1; :: thesis: verum

end;

A12: for A being Subset of the carrier' of C st A in D holds
for a being Attribute of C st a in A holds
x is-connected-with a

proof

let A be Subset of the carrier' of C; :: thesis: ( A in D implies for a being Attribute of C st a in A holds
x is-connected-with a )
assume A13: A in D ; :: thesis: for a being Attribute of C st a in A holds
x is-connected-with a
let a be Attribute of C; :: thesis: ( a in A implies x is-connected-with a )
assume A14: a in A ; :: thesis: x is-connected-with a
x in (AttributeDerivation C) . A by A11, A13;
then 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 } by CONLAT_1:def 7;
then consider x' being Object of C such that
A15: ( x' = x & ( for a being Attribute of C st a in A holds
x' is-connected-with a ) ) ;
thus x is-connected-with a by A14, A15; :: thesis: verum

end;

for a being Attribute of C st a in union D holds
x is-connected-with a

proof

let a be Attribute of C; :: thesis: ( a in union D implies x is-connected-with a )
assume a in union D ; :: thesis: x is-connected-with a
then consider Y being set such that
A16: ( a in Y & Y in D ) by TARSKI:def 4;
thus x is-connected-with a by A12, A16; :: thesis: verum

end;

then x in { o' where o' is Object of C : for a being Attribute of C st a in union D' holds
o' is-connected-with a } ;
hence x in (AttributeDerivation C) . (union D) by CONLAT_1:def 7; :: thesis: verum

end;

end;

case A17: { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = {} ; :: thesis: (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }

D = {}

proof

assume D <> {} ; :: thesis: contradiction
consider x being Element of D;
(AttributeDerivation C) . x in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ;
hence contradiction by A17; :: thesis: verum

end;

hence (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; :: thesis: verum

end;

end;

end;

hence (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; :: thesis: verum