consider A being non empty set , b1, b2, b3 being BinOp of A, e1, e2 being Element of A;
take Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) ; :: thesis: not Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) is empty
thus not the carrier of Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum