let X be set ; :: thesis: for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent
let F be Subset-Family of X; :: thesis: F, COMPLEMENT F are_equipotent
deffunc H₁( set ) -> Element of bool X = X \ $1;
consider f being Function such that
A1: dom f = F and
A2: for x being set st x in F holds
f . x = H₁(x) from FUNCT_1:sch 5();
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = F & rng f = COMPLEMENT F )
thus f is one-to-one :: thesis: ( dom f = F & rng f = COMPLEMENT F )

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider X1 = x1, X2 = x2 as Subset of X by A1, A3, A4;
X1 ` = f . x1 by A1, A2, A3
.= X2 ` by A1, A2, A4, A5 ;
hence x1 = (X2 `) `
.= x2 ;
:: thesis: verum

end;

thus dom f = F by A1; :: thesis: rng f = COMPLEMENT F
thus rng f c= COMPLEMENT F :: according to XBOOLE_0:def 10 :: thesis: COMPLEMENT F c= rng f

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng f or e in COMPLEMENT F )
assume e in rng f ; :: thesis: e in COMPLEMENT F
then consider u being object such that
A6: u in dom f and
A7: e = f . u by FUNCT_1:def 3;
reconsider Y = u as Subset of X by A1, A6;
e = Y ` by A1, A2, A6, A7;
hence e in COMPLEMENT F by A1, A6, SETFAM_1:35; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in COMPLEMENT F or e in rng f )
assume A8: e in COMPLEMENT F ; :: thesis: e in rng f
then reconsider Y = e as Subset of X ;
A9: Y ` in F by A8, SETFAM_1:def 7;
e = (Y `) `
.= f . (Y `) by A2, A9 ;
hence e in rng f by A1, A9, FUNCT_1:def 3; :: thesis: verum