let B, A 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 10;
hence Intersect G = x by SETFAM_1:11; :: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in G or a in {B} )
assume a in G ; :: thesis: a in {B}
then consider R being Subset of [:A,B:] such that
A5: ( a = R .:^ X & R in FR ) by A1;
a = B by A3, A5, Th29;
hence a in {B} by TARSKI:def 1; :: thesis: verum

end;

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

end;

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

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

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

then Intersect FR = [:A,B:] by SETFAM_1:def 10;
then A8: (Intersect FR) .:^ X = B by Th38;
G c= {B}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in G or a in {B} )
assume a in G ; :: thesis: a in {B}
then consider R being Subset of [:A,B:] such that
A9: ( a = R .:^ X & R in FR ) by A1;
thus a in {B} by A7, A9; :: thesis: verum

end;

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

end;

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

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

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

then [:A,B:] = {} by ZFMISC_1:113;
then ( FR = {} or FR = {{} } ) by ZFMISC_1:1, ZFMISC_1:39;
then Intersect FR = meet {{} } by A10, SETFAM_1:def 10;
then A13: (Intersect FR) .:^ X = {} by A6, Th37, SETFAM_1:11;
thus (Intersect FR) .:^ X = Intersect G by A11, A13; :: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in (Intersect FR) .:^ X or a in Intersect G )
assume A15: a in (Intersect FR) .:^ X ; :: thesis: a in Intersect G
then A16: a in B ;
reconsider a = a as Element of B by A15;
( G <> {} implies a in Intersect G )

proof

assume A17: G <> {} ; :: thesis: a in Intersect G
then A18: Intersect G = meet G by SETFAM_1:def 10;
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 A19: Y in G ; :: thesis: a in Y
consider R being Subset of [:A,B:] such that
A20: ( Y = R .:^ X & R in FR ) by A1, A19;
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 A21: x in X ; :: thesis: a in Im R,x
a in Im (Intersect FR),x by A15, A21, Th24;
then [x,a] in Intersect FR by Th9;
then [x,a] in meet FR by A10, SETFAM_1:def 10;
then [x,a] in R by A20, SETFAM_1:def 1;
hence a in Im R,x by Th9; :: thesis: verum

end;

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

end;

hence a in Intersect G by A17, A18, SETFAM_1:def 1; :: thesis: verum

end;

hence a in Intersect G by A16, SETFAM_1:def 10; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Intersect G or a in (Intersect FR) .:^ X )
assume A22: 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
A23: R in FR by A10, SUBSET_1:10;
R .:^ X in G by A1, A23;
then A24: a in meet G by A22, SETFAM_1:def 10;
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 A25: 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 A26: 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, A26;
then a in P .:^ X by A24, SETFAM_1:def 1;
then a in Im P,x by A25, Th24;
hence [x,a] in P by Th9; :: thesis: verum

end;

then [x,a] in meet FR by A10, SETFAM_1:def 1;
then [x,a] in Intersect FR by A10, SETFAM_1:def 10;
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;