let X be set ; :: thesis: for A being Subset-Family of X
for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds
INTERSECTION (a,b) c= FinMeetCl A
let A be Subset-Family of X; :: thesis: for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds
INTERSECTION (a,b) c= FinMeetCl A
let a, b be set ; :: thesis: ( a c= FinMeetCl A & b c= FinMeetCl A implies INTERSECTION (a,b) c= FinMeetCl A )
assume A1: ( a c= FinMeetCl A & b c= FinMeetCl A ) ; :: thesis: INTERSECTION (a,b) c= FinMeetCl A
let Z be object ; :: according to TARSKI:def 3 :: thesis: ( not Z in INTERSECTION (a,b) or Z in FinMeetCl A )
assume Z in INTERSECTION (a,b) ; :: thesis: Z in FinMeetCl A
then consider V, B being set such that
A2: ( V in a & B in b ) and
A3: Z = V /\ B by SETFAM_1:def 5;
( V in FinMeetCl A & B in FinMeetCl A ) by A1, A2;
then reconsider M = {V,B} as Subset-Family of X by ZFMISC_1:32;
reconsider M = M as Subset-Family of X ;
V /\ B = meet M by SETFAM_1:11;
then A4: V /\ B = Intersect M by SETFAM_1:def 9;
M c= FinMeetCl A by A1, A2, ZFMISC_1:32;
then Intersect M in FinMeetCl (FinMeetCl A) by Def3;
hence Z in FinMeetCl A by A3, A4, Th11; :: thesis: verum