set Bo = {} ;
consider yo being Function of {},A;
take cylinder0 (A,B,{},yo) ; :: thesis: ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & cylinder0 (A,B,{},yo) = cylinder0 (A,B,Bo,yo) )
{} is Subset of B by XBOOLE_1:2;
hence ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & cylinder0 (A,B,{},yo) = cylinder0 (A,B,Bo,yo) ) ; :: thesis: verum