let C be FormalContext; :: thesis: for O1, O2 being Subset of the carrier of C holds (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
let O1, O2 be Subset of the carrier of C; :: thesis: (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
reconsider O9 = O1 \/ O2 as Subset of the carrier of C ;
A1: for x being object st x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) holds
x in (ObjectDerivation C) . O9
proof
let x be object ; :: thesis: ( x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) implies x in (ObjectDerivation C) . O9 )
assume A2: x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) ; :: thesis: x in (ObjectDerivation C) . O9
then x in (ObjectDerivation C) . O1 by XBOOLE_0:def 4;
then x in { a where a is Attribute of C : for o being Object of C st o in O1 holds
o is-connected-with a } by Def2;
then A3: ex x1 being Attribute of C st
( x1 = x & ( for o being Object of C st o in O1 holds
o is-connected-with x1 ) ) ;
x in (ObjectDerivation C) . O2 by A2, XBOOLE_0:def 4;
then x in { a where a is Attribute of C : for o being Object of C st o in O2 holds
o is-connected-with a } by Def2;
then A4: ex x2 being Attribute of C st
( x2 = x & ( for o being Object of C st o in O2 holds
o is-connected-with x2 ) ) ;
then reconsider x = x as Attribute of C ;
for o being Object of C st o in O1 \/ O2 holds
o is-connected-with x
proof
let o be Object of C; :: thesis: ( o in O1 \/ O2 implies o is-connected-with x )
assume A5: o in O1 \/ O2 ; :: thesis: o is-connected-with x
hence o is-connected-with x ; :: thesis: verum
end;
then x in { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ;
hence x in (ObjectDerivation C) . O9 by Def2; :: thesis: verum
end;
for x being object st x in (ObjectDerivation C) . (O1 \/ O2) holds
x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
proof
let x be object ; :: thesis: ( x in (ObjectDerivation C) . (O1 \/ O2) implies x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) )
assume x in (ObjectDerivation C) . (O1 \/ O2) ; :: thesis: x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
then x in { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } by Def2;
then A6: ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O9 holds
o is-connected-with x9 ) ) ;
then reconsider x = x as Attribute of C ;
for o being Object of C st o in O2 holds
o is-connected-with x
proof
let o be Object of C; :: thesis: ( o in O2 implies o is-connected-with x )
assume o in O2 ; :: thesis: o is-connected-with x
then o in O9 by XBOOLE_0:def 3;
hence o is-connected-with x by A6; :: thesis: verum
end;
then x in { a where a is Attribute of C : for o being Object of C st o in O2 holds
o is-connected-with a } ;
then A7: x in (ObjectDerivation C) . O2 by Def2;
for o being Object of C st o in O1 holds
o is-connected-with x
proof
let o be Object of C; :: thesis: ( o in O1 implies o is-connected-with x )
assume o in O1 ; :: thesis: o is-connected-with x
then o in O9 by XBOOLE_0:def 3;
hence o is-connected-with x by A6; :: thesis: verum
end;
then x in { a where a is Attribute of C : for o being Object of C st o in O1 holds
o is-connected-with a } ;
then x in (ObjectDerivation C) . O1 by Def2;
hence x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) by A7, XBOOLE_0:def 4; :: thesis: verum
end;
hence (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) by A1, TARSKI:2; :: thesis: verum