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