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 B c= C ; :: thesis: thin_cylinders A,B c= bool (PFuncs C,A)
then A1: PFuncs B,A c= PFuncs C,A by PARTFUN1:128;
Funcs B,A c= PFuncs B,A by FUNCT_2:141;
then Funcs B,A c= PFuncs C,A by A1, XBOOLE_1:1;
then A2: bool (Funcs B,A) c= bool (PFuncs C,A) by ZFMISC_1:79;
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
A3: x = D and
D is thin_cylinder of A,B ;
D in bool (Funcs B,A) ;
hence x in bool (PFuncs C,A) by A3, A2; :: thesis: verum