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

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

suppose A1: { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } <> {} ; :: thesis: (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D }

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

proof

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

proof

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

end;

A5: for O being Subset of the carrier of C st O in D holds
x in (ObjectDerivation C) . O

proof

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

end;

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

proof

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

end;

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

end;

thus meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } c= (ObjectDerivation C) . (union D) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } or x in (ObjectDerivation C) . (union D) )
assume A7: x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ; :: thesis: x in (ObjectDerivation C) . (union D)
consider d being Element of { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ;
A8: d in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O 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 = (ObjectDerivation C) . X & X in D ) by A8;
reconsider x = x as Attribute of C by A9, A10;
A11: for O being Subset of the carrier of C st O in D holds
x in (ObjectDerivation C) . O

proof

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

end;

A12: for O being Subset of the carrier of C st O in D holds
for o being Object of C st o in O holds
o is-connected-with x

proof

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

end;

for o being Object of C st o in union D holds
o is-connected-with x

proof

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

end;

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

end;

end;

suppose A17: { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } = {} ; :: thesis: (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D }

D = {}

proof

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

end;

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

end;

end;