let A be finite set ; :: thesis: for X being non empty Subset-Family of A ex C being Element of X st
for B being Element of X st B c= C holds
B = C
let X be non empty Subset-Family of A; :: thesis: ex C being Element of X st
for B being Element of X st B c= C holds
B = C
reconsider D = COMPLEMENT X as non empty Subset-Family of A by SETFAM_1:32;
consider x being set such that
A1: x in D and
A2: for B being set st B in D & x c= B holds
B = x by FINSET_1:6;
reconsider x = x as Subset of A by A1;
reconsider C = x ` as Element of X by A1, SETFAM_1:def 7;
take C ; :: thesis: for B being Element of X st B c= C holds
B = C
let B be Element of X; :: thesis: ( B c= C implies B = C )
assume A3: B c= C ; :: thesis: B = C
(B `) ` = B ;
then B ` in D by SETFAM_1:def 7;
then B ` = x by A2, A3, SUBSET_1:16;
hence B = C ; :: thesis: verum