set X = the infinite set ;
set Z = the Element of the infinite set ;
set O = the Element of the infinite set \ { the Element of the infinite set };
reconsider Y = the infinite set \ { the Element of the infinite set } as infinite set ;
not the Element of the infinite set \ { the Element of the infinite set } in { the Element of the infinite set } by XBOOLE_0:def 5;
then A1: the Element of the infinite set \ { the Element of the infinite set } <> the Element of the infinite set by TARSKI:def 1;
reconsider OO = the Element of the infinite set \ { the Element of the infinite set } as Element of the infinite set ;
set S = ZeroOneStr(# the infinite set , the Element of the infinite set ,OO #);
( 1. ZeroOneStr(# the infinite set , the Element of the infinite set ,OO #) = OO & 0. ZeroOneStr(# the infinite set , the Element of the infinite set ,OO #) = the Element of the infinite set ) ;
then reconsider SS = ZeroOneStr(# the infinite set , the Element of the infinite set ,OO #) as non degenerated ZeroOneStr by A1, STRUCT_0:def 8;
take SS ; :: thesis: SS is infinite
thus SS is infinite ; :: thesis: verum