set C = the non empty set ;
set O = the non empty set ;
set ay = the Function of the non empty set ,( the non empty set *);
set rs = the Function of the non empty set , the non empty set ;
set f = the Element of the non empty set ;
set p = the Element of the non empty set ;
set c = the FinSequence of the non empty set ;
set qs = {1,2};
set q = the Function of [:{1,2},X:], the non empty set ;
take L = AlgLangSignature(# the non empty set , the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set , the Element of the non empty set , the Element of the non empty set , the FinSequence of the non empty set ,{1,2}, the Function of [:{1,2},X:], the non empty set #); :: thesis: ( not L is void & not L is empty )
thus not the carrier' of L is empty ; :: according to STRUCT_0:def 13 :: thesis: not L is empty
thus not the carrier of L is empty ; :: according to STRUCT_0:def 1 :: thesis: verum