thus not the BasicAssign of (Inf_seqModel S,BASSIGN) is empty ; :: according to MODELC_2:def 30 :: thesis: ( Inf_seqModel S,BASSIGN is strict & not Inf_seqModel S,BASSIGN is empty )
thus ( Inf_seqModel S,BASSIGN is strict & not Inf_seqModel S,BASSIGN is empty ) ; :: thesis: verum