let A be non empty set ; for B, C being set st B c= C holds
thin_cylinders (A,B) c= bool (PFuncs (C,A))
let B, C be set ; ( B c= C implies thin_cylinders (A,B) c= bool (PFuncs (C,A)) )
assume
B c= C
; thin_cylinders (A,B) c= bool (PFuncs (C,A))
then A1:
PFuncs (B,A) c= PFuncs (C,A)
by PARTFUN1:50;
Funcs (B,A) c= PFuncs (B,A)
by FUNCT_2:72;
then
Funcs (B,A) c= PFuncs (C,A)
by A1;
then A2:
bool (Funcs (B,A)) c= bool (PFuncs (C,A))
by ZFMISC_1:67;
let x be object ; TARSKI:def 3 ( not x in thin_cylinders (A,B) or x in bool (PFuncs (C,A)) )
assume
x in thin_cylinders (A,B)
; x in bool (PFuncs (C,A))
then consider D being Subset of (Funcs (B,A)) such that
A3:
x = D
and
D is thin_cylinder of A,B
;
thus
x in bool (PFuncs (C,A))
by A3, A2; verum