let A, B be set ; :: thesis: for X being Subset of A
for FR being Subset-Family of [:A,B:]
for G being Subset-Family of B st G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } holds
(Intersect FR) .:^ X = Intersect G
let X be Subset of A; :: thesis: for FR being Subset-Family of [:A,B:]
for G being Subset-Family of B st G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } holds
(Intersect FR) .:^ X = Intersect G
let FR be Subset-Family of [:A,B:]; :: thesis: for G being Subset-Family of B st G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } holds
(Intersect FR) .:^ X = Intersect G
let G be Subset-Family of B; :: thesis: ( G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } implies (Intersect FR) .:^ X = Intersect G )
assume A1: G = { (R .:^ X) where R is Subset of [:A,B:] : R in FR } ; :: thesis: (Intersect FR) .:^ X = Intersect G
A2: for x being set st G = {x} holds
Intersect G = x

proof

let x be set ; :: thesis: ( G = {x} implies Intersect G = x )
assume G = {x} ; :: thesis: Intersect G = x
then Intersect G = meet {x} by SETFAM_1:def 9;
hence Intersect G = x by SETFAM_1:10; :: thesis: verum

end;

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

suppose A3: X = {} ; :: thesis: (Intersect FR) .:^ X = Intersect G

then A4: (Intersect FR) .:^ X = B by Th29;
G c= {B}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in G or a in {B} )
assume a in G ; :: thesis: a in {B}
then ex R being Subset of [:A,B:] st
( a = R .:^ X & R in FR ) by A1;
then a = B by A3, Th29;
hence a in {B} by TARSKI:def 1; :: thesis: verum

end;

then ( G = {} or G = {B} ) by ZFMISC_1:33;
hence (Intersect FR) .:^ X = Intersect G by A2, A4, SETFAM_1:def 9; :: thesis: verum

end;

suppose A5: X <> {} ; :: thesis: (Intersect FR) .:^ X = Intersect G

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

suppose A6: FR = {} ; :: thesis: (Intersect FR) .:^ X = Intersect G

then Intersect FR = [:A,B:] by SETFAM_1:def 9;
then A7: (Intersect FR) .:^ X = B by Th37;
G c= {B}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in G or a in {B} )
assume a in G ; :: thesis: a in {B}
then ex R being Subset of [:A,B:] st
( a = R .:^ X & R in FR ) by A1;
hence a in {B} by A6; :: thesis: verum

end;

then ( G = {} or G = {B} ) by ZFMISC_1:33;
hence (Intersect FR) .:^ X = Intersect G by A2, A7, SETFAM_1:def 9; :: thesis: verum

end;

suppose A8: FR <> {} ; :: thesis: (Intersect FR) .:^ X = Intersect G

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

suppose A9: B = {} ; :: thesis: (Intersect FR) .:^ X = Intersect G

then [:A,B:] = {} by ZFMISC_1:90;
then ( FR = {} or FR = {{}} ) by ZFMISC_1:1, ZFMISC_1:33;
then Intersect FR = meet {{}} by A8, SETFAM_1:def 9;
then (Intersect FR) .:^ X = {} by A5, Th36, SETFAM_1:10;
hence (Intersect FR) .:^ X = Intersect G by A9; :: thesis: verum

end;

suppose B <> {} ; :: thesis: (Intersect FR) .:^ X = Intersect G

then reconsider B = B as non empty set ;
thus (Intersect FR) .:^ X c= Intersect G :: according to XBOOLE_0:def 10 :: thesis: Intersect G c= (Intersect FR) .:^ X

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (Intersect FR) .:^ X or a in Intersect G )
assume A10: a in (Intersect FR) .:^ X ; :: thesis: a in Intersect G
then A11: a in B ;
reconsider a = a as Element of B by A10;
( G <> {} implies a in Intersect G )

proof

assume A12: G <> {} ; :: thesis: a in Intersect G
then A13: Intersect G = meet G by SETFAM_1:def 9;
for Y being set st Y in G holds
a in Y

proof

let Y be set ; :: thesis: ( Y in G implies a in Y )
assume Y in G ; :: thesis: a in Y
then consider R being Subset of [:A,B:] such that
A14: Y = R .:^ X and
A15: R in FR by A1;
for x being set st x in X holds
a in Im (R,x)

proof

let x be set ; :: thesis: ( x in X implies a in Im (R,x) )
assume x in X ; :: thesis: a in Im (R,x)
then a in Im ((Intersect FR),x) by A10, Th24;
then [x,a] in Intersect FR by Th9;
then [x,a] in meet FR by A8, SETFAM_1:def 9;
then [x,a] in R by A15, SETFAM_1:def 1;
hence a in Im (R,x) by Th9; :: thesis: verum

end;

hence a in Y by A14, Th25; :: thesis: verum

end;

hence a in Intersect G by A12, A13, SETFAM_1:def 1; :: thesis: verum

end;

hence a in Intersect G by A11, 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 (Intersect FR) .:^ X )
assume A16: a in Intersect G ; :: thesis: a in (Intersect FR) .:^ X
then reconsider a = a as Element of B ;
consider R being Subset of [:A,B:] such that
A17: R in FR by A8, SUBSET_1:4;
R .:^ X in G by A1, A17;
then A18: a in meet G by A16, SETFAM_1:def 9;
for x being set st x in X holds
a in Im ((Intersect FR),x)

proof

let x be set ; :: thesis: ( x in X implies a in Im ((Intersect FR),x) )
assume A19: x in X ; :: thesis: a in Im ((Intersect FR),x)
for Y being set st Y in FR holds
[x,a] in Y

proof

let P be set ; :: thesis: ( P in FR implies [x,a] in P )
assume A20: P in FR ; :: thesis: [x,a] in P
then reconsider P = P as Subset of [:A,B:] ;
set S = P .:^ X;
P .:^ X in G by A1, A20;
then a in P .:^ X by A18, SETFAM_1:def 1;
then a in Im (P,x) by A19, Th24;
hence [x,a] in P by Th9; :: thesis: verum

end;

then [x,a] in meet FR by A8, SETFAM_1:def 1;
then [x,a] in Intersect FR by A8, SETFAM_1:def 9;
hence a in Im ((Intersect FR),x) by Th9; :: thesis: verum

end;

hence a in (Intersect FR) .:^ X by Th25; :: thesis: verum

end;

end;

end;

end;

end;

end;