let X be set ; :: thesis: for A being Subset-Family of X holds A c= FinMeetCl A
let A be Subset-Family of X; :: thesis: A c= FinMeetCl A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in FinMeetCl A )
assume A1: x in A ; :: thesis: x in FinMeetCl A
then reconsider x9 = x as Subset of X ;
reconsider s = {x9} as Subset-Family of X by SUBSET_1:41;
x = meet s by SETFAM_1:10;
then A2: x = Intersect s by SETFAM_1:def 9;
s c= A by A1, ZFMISC_1:31;
hence x in FinMeetCl A by A2, Def3; :: thesis: verum