let A be non empty set ; :: thesis: for B, C being set st B c= C holds
thin_cylinders A,B c= bool (PFuncs C,A)
let B, C be set ; :: thesis: ( B c= C implies thin_cylinders A,B c= bool (PFuncs C,A) )
assume AS: B c= C ; :: thesis: thin_cylinders A,B c= bool (PFuncs C,A)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in thin_cylinders A,B or x in bool (PFuncs C,A) )
assume x in thin_cylinders A,B ; :: thesis: x in bool (PFuncs C,A)
then consider D being Subset of (Funcs B,A) such that
P1: ( x = D & D is thin_cylinder of A,B ) ;
P2: D in bool (Funcs B,A) ;
P3: Funcs B,A c= PFuncs B,A by FUNCT_2:141;
PFuncs B,A c= PFuncs C,A by AS, PARTFUN1:128;
then Funcs B,A c= PFuncs C,A by P3, XBOOLE_1:1;
then bool (Funcs B,A) c= bool (PFuncs C,A) by ZFMISC_1:79;
hence x in bool (PFuncs C,A) by P1, P2; :: thesis: verum