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

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

end;

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

end;

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

end;

end;

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

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