let A1, A2 be non empty set ; :: thesis: for B being set
for D1 being thin_cylinder of A1,B st A1 c= A2 holds
ex D2 being thin_cylinder of A2,B st D1 c= D2
let B be set ; :: thesis: for D1 being thin_cylinder of A1,B st A1 c= A2 holds
ex D2 being thin_cylinder of A2,B st D1 c= D2
let D1 be thin_cylinder of A1,B; :: thesis: ( A1 c= A2 implies ex D2 being thin_cylinder of A2,B st D1 c= D2 )
consider Bo being Subset of B, yo1 being Function of Bo,A1 such that
A1: Bo is finite and
A2: D1 = { y where y is Function of B,A1 : y | Bo = yo1 } by Th1;
assume A3: A1 c= A2 ; :: thesis: ex D2 being thin_cylinder of A2,B st D1 c= D2
then reconsider yo2 = yo1 as Function of Bo,A2 by FUNCT_2:7;
set D2 = { y where y is Function of B,A2 : y | Bo = yo2 } ;
A4: now :: thesis: for x being object st x in D1 holds
x in { y where y is Function of B,A2 : y | Bo = yo2 }
let x be object ; :: thesis: ( x in D1 implies x in { y where y is Function of B,A2 : y | Bo = yo2 } )
assume x in D1 ; :: thesis: x in { y where y is Function of B,A2 : y | Bo = yo2 }
then consider y1 being Function of B,A1 such that
A5: x = y1 and
A6: y1 | Bo = yo1 by A2;
reconsider y2 = y1 as Function of B,A2 by A3, FUNCT_2:7;
y2 | Bo = yo1 by A6;
hence x in { y where y is Function of B,A2 : y | Bo = yo2 } by A5; :: thesis: verum
end;
{ y where y is Function of B,A2 : y | Bo = yo2 } = cylinder0 (A2,B,Bo,yo2) by Def1;
then reconsider D2 = { y where y is Function of B,A2 : y | Bo = yo2 } as thin_cylinder of A2,B by A1, Def2;
take D2 ; :: thesis: D1 c= D2
thus D1 c= D2 by A4; :: thesis: verum