let S be non empty set ; for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
let R be total Relation of S,S; for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
let s be Element of S; for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
let BASSIGN be non empty Subset of (ModelSP S); for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
let f, g be Assign of (BASSModel (R,BASSIGN)); ( s |= f 'or' g iff ( s |= f or s |= g ) )
( s |= f 'or' g iff not s |= ('not' f) '&' ('not' g) )
by Th12;
then
( s |= f 'or' g iff ( not s |= 'not' f or not s |= 'not' g ) )
by Th13;
hence
( s |= f 'or' g iff ( s |= f or s |= g ) )
by Th12; verum