let T be TopSpace; :: thesis: for A being Subset of T
for F being Subset-Family of T holds card (F | A) c= card F
let A be Subset of T; :: thesis: for F being Subset-Family of T holds card (F | A) c= card F
let F be Subset-Family of T; :: thesis: card (F | A) c= card F
set FA = F | A;

per cases ( F | A is empty or not F | A is empty ) ;

suppose F | A is empty ; :: thesis: card (F | A) c= card F

hence card (F | A) c= card F ; :: thesis: verum

end;

suppose A1: not F | A is empty ; :: thesis: card (F | A) c= card F

deffunc H₁( set ) -> Element of bool the carrier of T = $1 /\ A;
A2: A = [#] (T | A) by PRE_TOPC:def 5;
A3: for x being set st x in F holds
H₁(x) in F | A

proof

let x be set ; :: thesis: ( x in F implies H₁(x) in F | A )
A4: H₁(x) c= A by XBOOLE_1:17;
assume x in F ; :: thesis: H₁(x) in F | A
hence H₁(x) in F | A by A2, A4, TOPS_2:def 3; :: thesis: verum

end;

consider g being Function of F,(F | A) such that
A5: for x being set st x in F holds
g . x = H₁(x) from FUNCT_2:sch 11(A3);
A6: dom g = F by A1, FUNCT_2:def 1;
F | A c= rng g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F | A or x in rng g )
assume x in F | A ; :: thesis: x in rng g
then consider B being Subset of T such that
A7: B in F and
A8: H₁(B) = x by TOPS_2:def 3;
x = g . B by A5, A7, A8;
hence x in rng g by A6, A7, FUNCT_1:def 3; :: thesis: verum

end;

hence card (F | A) c= card F by A6, CARD_1:12; :: thesis: verum

end;

end;