set Bo = {} ;
consider yo being Function of {} ,A;
take D = cylinder0 A,B,{} ,yo; :: thesis: ex Bo being Subset of B ex yo being Function of Bo,A st
( Bo is finite & D = 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 & D = cylinder0 A,B,Bo,yo ) ; :: thesis: verum