let X be set ; :: thesis: for A being Subset-Family of X st X in A holds
for x being set holds
( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) )
let A be Subset-Family of X; :: thesis: ( X in A implies for x being set holds
( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) ) )
assume A1: X in A ; :: thesis: for x being set holds
( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) )
then A2: {X} c= A by ZFMISC_1:31;
reconsider Z = {X} as non empty finite Subset-Family of X by A1, ZFMISC_1:31;
reconsider Z = Z as non empty finite Subset-Family of X ;
A3: Intersect Z = meet Z by SETFAM_1:def 9
.= X by SETFAM_1:10 ;
let x be set ; :: thesis: ( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) )

hereby :: thesis: ( ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) implies x in FinMeetCl A )

assume x in FinMeetCl A ; :: thesis: ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y )
then consider Y being Subset-Family of X such that
A4: Y c= A and
A5: Y is finite and
A6: x = Intersect Y by CANTOR_1:def 3;

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y )

then x = X by A6, SETFAM_1:def 9;
hence ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) by A2, A3; :: thesis: verum

end;

suppose Y <> {} ; :: thesis: ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y )

hence ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) by A4, A5, A6; :: thesis: verum

end;

end;

end;

thus ( ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) implies x in FinMeetCl A ) by CANTOR_1:def 3; :: thesis: verum