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 D9 = 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 :: thesis: ( ( { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } <> {} & (AttributeDerivation C) . (union D) = meet { ((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 } = {} & (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ) )

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 object ; :: 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 { o9 where o9 is Object of C : for a being Attribute of C st a in union D9 holds
o9 is-connected-with a } by CONLAT_1:def 4;
then A2: ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in union D holds
x9 is-connected-with a ) ) ;
then reconsider x = x as Object of C ;
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 4; :: 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 ex A being Subset of the carrier' of C st
( Y = (AttributeDerivation C) . A & A in D ) ;
hence x in Y by A5; :: 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;

set d = the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ;
let x be object ; :: 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 A6: 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)
then A7: x in the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } by A1, SETFAM_1:def 1;
the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } by A1;
then ex X being Subset of the carrier' of C st
( the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = (AttributeDerivation C) . X & X in D ) ;
then reconsider x = x as Object of C by A7;
A8: 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) . A9) where A9 is Subset of the carrier' of C : A9 in D } ;
hence x in (AttributeDerivation C) . A by A6, SETFAM_1:def 1; :: thesis: verum

end;

A9: 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 A in D ; :: thesis: for a being Attribute of C st a in A holds
x is-connected-with a
then x in (AttributeDerivation C) . A by A8;
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 4;
then A10: 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 ) ) ;
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
hence x is-connected-with a by A10; :: 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 ex Y being set st
( a in Y & Y in D ) by TARSKI:def 4;
hence x is-connected-with a by A9; :: thesis: verum

end;

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

end;

end;

case A11: { ((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

set x = the Element of D;
assume D <> {} ; :: thesis: contradiction
(AttributeDerivation C) . the Element of D in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ;
hence contradiction by A11; :: 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