let X be set ; :: thesis: for A being Subset-Family of X
for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds
a /\ b in FinMeetCl A
let A be Subset-Family of X; :: thesis: for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds
a /\ b in FinMeetCl A
let a, b be set ; :: thesis: ( a in FinMeetCl A & b in FinMeetCl A implies a /\ b in FinMeetCl A )
assume A1: ( a in FinMeetCl A & b in FinMeetCl A ) ; :: thesis: a /\ b in FinMeetCl A
then reconsider M = {a,b} as Subset-Family of X by ZFMISC_1:32;
reconsider M = M as Subset-Family of X ;
a /\ b = meet M by SETFAM_1:11;
then A2: a /\ b = Intersect M by SETFAM_1:def 9;
M c= FinMeetCl A by A1, ZFMISC_1:32;
then Intersect M in FinMeetCl (FinMeetCl A) by Def3;
hence a /\ b in FinMeetCl A by A2, Th11; :: thesis: verum