let T be 1-sorted ; :: thesis: for F being Subset-Family of T st COMPLEMENT F is finite holds
F is finite
let F be Subset-Family of T; :: thesis: ( COMPLEMENT F is finite implies F is finite )
defpred S₁[ object , object ] means for X being Subset of T st X = $1 holds
$2 = X ` ;
A1: for x being object st x in COMPLEMENT F holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in COMPLEMENT F implies ex y being object st S₁[x,y] )
assume x in COMPLEMENT F ; :: thesis: ex y being object st S₁[x,y]
then reconsider X = x as Subset of T ;
reconsider y = X ` as object ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A2: dom f = COMPLEMENT F and
A3: for x being object st x in COMPLEMENT F holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
for x being object holds
( x in rng f iff x in F )

proof

let x be object ; :: thesis: ( x in rng f iff x in F )

hereby :: thesis: ( x in F implies x in rng f )

assume x in rng f ; :: thesis: x in F
then consider y being object such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def 3;
reconsider Y = y as Subset of T by A2, A4;
Y ` in F by A2, A4, SETFAM_1:def 7;
hence x in F by A2, A3, A4, A5; :: thesis: verum

end;

assume A6: x in F ; :: thesis: x in rng f
then reconsider X = x as Subset of T ;
A7: (X `) ` = X ;
then X ` in COMPLEMENT F by A6, SETFAM_1:def 7;
then A8: f . (X `) = (X `) ` by A3;
X ` in dom f by A2, A6, A7, SETFAM_1:def 7;
hence x in rng f by A8, FUNCT_1:def 3; :: thesis: verum

end;

then rng f = F by TARSKI:2;
then A9: f .: (COMPLEMENT F) = F by A2, RELAT_1:113;
assume COMPLEMENT F is finite ; :: thesis: F is finite
hence F is finite by A9, FINSET_1:5; :: thesis: verum