theorem :: MODELC_2:56

for S being non empty set
for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))
for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( f 'or' g = 'not' (('not' f) '&' ('not' g)) & f 'R' g = 'not' (('not' f) 'U' ('not' g)) ) by Def54, Def55;