let S be non empty set ; :: thesis: for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))
for t being Element of Inf_seq S
for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f 'or' g iff ( t |= f or t |= g ) )
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); :: thesis: for t being Element of Inf_seq S
for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f 'or' g iff ( t |= f or t |= g ) )
let t be Element of Inf_seq S; :: thesis: for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f 'or' g iff ( t |= f or t |= g ) )
let f, g be Assign of (Inf_seqModel (S,BASSIGN)); :: thesis: ( t |= f 'or' g iff ( t |= f or t |= g ) )
( t |= f 'or' g iff t |= 'not' (('not' f) '&' ('not' g)) ) by Def54;
then ( t |= f 'or' g iff not t |= ('not' f) '&' ('not' g) ) by Th57;
then ( t |= f 'or' g iff ( not t |= 'not' f or not t |= 'not' g ) ) by Th58;
hence ( t |= f 'or' g iff ( t |= f or t |= g ) ) by Th57; :: thesis: verum