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: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 ; :: 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 ;
thus x in bool (PFuncs (C,A)) by A3, A2; :: thesis: verum