consider A being non empty set , a being BinOp of A, Z being Element of A, l being Function of [: the carrier of FS1,A:],A, r being Function of [:A, the carrier of FS2:],A;
take BiModStr(# A,a,Z,l,r #) ; :: thesis: not BiModStr(# A,a,Z,l,r #) is empty
thus not the carrier of BiModStr(# A,a,Z,l,r #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum