let A be set ; :: thesis: for B being non empty set
for R being Relation of A,B
for F being Subset-Family of A
for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
let B be non empty set ; :: thesis: for R being Relation of A,B
for F being Subset-Family of A
for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
let R be Relation of A,B; :: thesis: for F being Subset-Family of A
for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
let F be Subset-Family of A; :: thesis: for G being Subset-Family of B st G = { (R .:^ Y) where Y is Subset of A : Y in F } holds
R .:^ (union F) = Intersect G
let G be Subset-Family of B; :: thesis: ( G = { (R .:^ Y) where Y is Subset of A : Y in F } implies R .:^ (union F) = Intersect G )
assume A1: G = { (R .:^ Y) where Y is Subset of A : Y in F } ; :: thesis: R .:^ (union F) = Intersect G

per cases ( union F = {} or union F <> {} ) ;

suppose A2: union F = {} ; :: thesis: R .:^ (union F) = Intersect G

then A3: R .:^ (union F) = B by Th29;

per cases ( G <> {} or G = {} ) ;

suppose A4: G <> {} ; :: thesis: R .:^ (union F) = Intersect G

G c= {B}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in {B} )
assume x in G ; :: thesis: x in {B}
then consider Y being Subset of A such that
A5: x = R .:^ Y and
A6: Y in F by A1;
Y = {} by A2, A6, ORDERS_1:6;
then (.: R) .: {_{Y}_} = {} by Th23;
then Intersect ((.: R) .: {_{Y}_}) = B by SETFAM_1:def 9;
hence x in {B} by A5, TARSKI:def 1; :: thesis: verum

end;

then meet {B} c= meet G by A4, SETFAM_1:6;
then B c= meet G by SETFAM_1:10;
then meet G = B ;
hence R .:^ (union F) = Intersect G by A3, SETFAM_1:def 9; :: thesis: verum

end;

suppose G = {} ; :: thesis: R .:^ (union F) = Intersect G

hence R .:^ (union F) = Intersect G by A3, SETFAM_1:def 9; :: thesis: verum

end;

end;

end;

suppose union F <> {} ; :: thesis: R .:^ (union F) = Intersect G

then consider Z1 being set such that
Z1 <> {} and
A7: Z1 in F by ORDERS_1:6;
reconsider Z1 = Z1 as Subset of A by A7;
A8: G <> {}

proof

assume not G <> {} ; :: thesis: contradiction
then not R .:^ Z1 in G ;
hence contradiction by A1, A7; :: thesis: verum

end;

thus R .:^ (union F) c= Intersect G :: according to XBOOLE_0:def 10 :: thesis: Intersect G c= R .:^ (union F)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in R .:^ (union F) or a in Intersect G )
assume A9: a in R .:^ (union F) ; :: thesis: a in Intersect G
for Y being set st Y in G holds
a in Y

proof

let Z2 be set ; :: thesis: ( Z2 in G implies a in Z2 )
assume Z2 in G ; :: thesis: a in Z2
then consider Z3 being Subset of A such that
A10: Z2 = R .:^ Z3 and
A11: Z3 in F by A1;
reconsider a = a as Element of B by A9;
for x being set st x in Z3 holds
a in Im (R,x)

proof

let x be set ; :: thesis: ( x in Z3 implies a in Im (R,x) )
assume x in Z3 ; :: thesis: a in Im (R,x)
then x in union F by A11, TARSKI:def 4;
hence a in Im (R,x) by A9, Th24; :: thesis: verum

end;

hence a in Z2 by A10, Th25; :: thesis: verum

end;

then a in meet G by A8, SETFAM_1:def 1;
hence a in Intersect G by A8, SETFAM_1:def 9; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Intersect G or a in R .:^ (union F) )
assume A12: a in Intersect G ; :: thesis: a in R .:^ (union F)
then A13: a in meet G by A8, SETFAM_1:def 9;
reconsider a = a as Element of B by A12;
for X being set st X in union F holds
a in Im (R,X)

proof

let X be set ; :: thesis: ( X in union F implies a in Im (R,X) )
assume X in union F ; :: thesis: a in Im (R,X)
then consider Z being set such that
A14: X in Z and
A15: Z in F by TARSKI:def 4;
reconsider Z = Z as Subset of A by A15;
set C = R .:^ Z;
R .:^ Z in G by A1, A15;
then a in R .:^ Z by A13, SETFAM_1:def 1;
hence a in Im (R,X) by A14, Th24; :: thesis: verum

end;

hence a in R .:^ (union F) by Th25; :: thesis: verum

end;

end;