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