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

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

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

thus (ObjectDerivation C) . (union D) c= meet { ((ObjectDerivation C) . O) where O is Subset of : O in D } :: according to XBOOLE_0:def 10 :: thesis: meet { ((ObjectDerivation C) . O) where O is Subset of : 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 : O in D } )
assume x in (ObjectDerivation C) . (union D) ; :: thesis: x in meet { ((ObjectDerivation C) . O) where O is Subset of : O in D }
then x in { a' where a' is Attribute of : for o being Object of st o in union D' holds
o is-connected-with a' } by CONLAT_1:def 6;
then A2: ex x' being Attribute of st
( x' = x & ( for o being Object of st o in union D holds
o is-connected-with x' ) ) ;
then reconsider x = x as Attribute of ;
A3: for O being Subset of st O in D holds
for o being Object of st o in O holds
o is-connected-with x

proof

let O be Subset of ; :: thesis: ( O in D implies for o being Object of st o in O holds
o is-connected-with x )
assume A4: O in D ; :: thesis: for o being Object of st o in O holds
o is-connected-with x
let o be Object of ; :: 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 st O in D holds
x in (ObjectDerivation C) . O

proof

let O be Subset of ; :: 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 st o in O holds
o is-connected-with x by A3;
then x in { a where a is Attribute of : for o being Object of 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 : O in D } holds
x in Y

proof

let Y be set ; :: thesis: ( Y in { ((ObjectDerivation C) . O) where O is Subset of : O in D } implies x in Y )
assume Y in { ((ObjectDerivation C) . O) where O is Subset of : O in D } ; :: thesis: x in Y
then ex O being Subset of 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 : O in D } by A1, SETFAM_1:def 1; :: thesis: verum

end;

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

proof

consider d being Element of { ((ObjectDerivation C) . O) where O is Subset of : O in D } ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { ((ObjectDerivation C) . O) where O is Subset of : O in D } or x in (ObjectDerivation C) . (union D) )
assume A6: x in meet { ((ObjectDerivation C) . O) where O is Subset of : O in D } ; :: thesis: x in (ObjectDerivation C) . (union D)
then A7: x in d by A1, SETFAM_1:def 1;
d in { ((ObjectDerivation C) . O) where O is Subset of : O in D } by A1;
then ex X being Subset of st
( d = (ObjectDerivation C) . X & X in D ) ;
then reconsider x = x as Attribute of by A7;
A8: for O being Subset of st O in D holds
x in (ObjectDerivation C) . O

proof

let O be Subset of ; :: 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 : O' in D } ;
hence x in (ObjectDerivation C) . O by A6, SETFAM_1:def 1; :: thesis: verum

end;

A9: for O being Subset of st O in D holds
for o being Object of st o in O holds
o is-connected-with x

proof

let O be Subset of ; :: thesis: ( O in D implies for o being Object of st o in O holds
o is-connected-with x )
assume O in D ; :: thesis: for o being Object of 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 : for o being Object of st o in O holds
o is-connected-with a } by CONLAT_1:def 6;
then A10: ex x' being Attribute of st
( x' = x & ( for o being Object of st o in O holds
o is-connected-with x' ) ) ;
let o be Object of ; :: 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 st o in union D holds
o is-connected-with x

proof

let o be Object of ; :: 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 { a' where a' is Attribute of : for o being Object of 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 A11: { ((ObjectDerivation C) . O) where O is Subset of : O in D } = {} ; :: thesis: (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of : O in D }

D = {}

proof

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

end;

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

end;

end;