let M be multMagma ; :: thesis: for F being Function st ( for i being set st i in dom F holds
F . i is stable Subset of M ) holds
meet F is stable Subset of M
let F be Function; :: thesis: ( ( for i being set st i in dom F holds
F . i is stable Subset of M ) implies meet F is stable Subset of M )
assume A1: for i being set st i in dom F holds
F . i is stable Subset of M ; :: thesis: meet F is stable Subset of M
A2: for x being object st x in meet F holds
x in the carrier of M

proof

let x be object ; :: thesis: ( x in meet F implies x in the carrier of M )
assume x in meet F ; :: thesis: x in the carrier of M
then A3: x in meet (rng F) by FUNCT_6:def 4;

per cases ( dom F is empty or not dom F is empty ) ;

suppose dom F is empty ; :: thesis: x in the carrier of M

then F = {} ;
hence x in the carrier of M by A3, SETFAM_1:1; :: thesis: verum

end;

suppose not dom F is empty ; :: thesis: x in the carrier of M

then consider i being object such that
A4: i in dom F by XBOOLE_0:def 1;
meet (rng F) c= F . i by A4, FUNCT_1:3, SETFAM_1:3;
then A5: x in F . i by A3;
F . i is stable Subset of M by A1, A4;
hence x in the carrier of M by A5; :: thesis: verum

end;

end;

end;

for v, w being Element of M st v in meet F & w in meet F holds
v * w in meet F

proof

let v, w be Element of M; :: thesis: ( v in meet F & w in meet F implies v * w in meet F )
assume A6: ( v in meet F & w in meet F ) ; :: thesis: v * w in meet F

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

suppose F = {} ; :: thesis: v * w in meet F

then meet (rng F) = {} by SETFAM_1:1;
hence v * w in meet F by A6, FUNCT_6:def 4; :: thesis: verum

end;

suppose A7: F <> {} ; :: thesis: v * w in meet F

A8: ( v in meet (rng F) & w in meet (rng F) ) by A6, FUNCT_6:def 4;
for Y being set st Y in rng F holds
v * w in Y

proof

let Y be set ; :: thesis: ( Y in rng F implies v * w in Y )
assume A9: Y in rng F ; :: thesis: v * w in Y
then A10: ( v in Y & w in Y ) by A8, SETFAM_1:def 1;
consider i being object such that
A11: ( i in dom F & Y = F . i ) by A9, FUNCT_1:def 3;
Y is stable Subset of M by A1, A11;
hence v * w in Y by A10, Def10; :: thesis: verum

end;

then v * w in meet (rng F) by A7, SETFAM_1:def 1;
hence v * w in meet F by FUNCT_6:def 4; :: thesis: verum

end;

end;

end;

hence meet F is stable Subset of M by A2, Def10, TARSKI:def 3; :: thesis: verum