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 x' = x as Subset of X ;
reconsider s = {x'} as Subset-Family of X by SUBSET_1:63;
reconsider s = s as Subset-Family of X ;
A2: ( s is finite & s c= A & x = meet s ) by A1, SETFAM_1:11, ZFMISC_1:37;
then x = Intersect s by SETFAM_1:def 10;
hence x in FinMeetCl A by A2, Def4; :: thesis: verum