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 set ; :: 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:63;
x = meet s by SETFAM_1:11;
then A2: x = Intersect s by SETFAM_1:def 10;
s c= A by A1, ZFMISC_1:37;
hence x in FinMeetCl A by A2, Def4; :: thesis: verum