let E be non empty set ; :: thesis: for f being Function of VAR ,E
for H, H' being ZF-formula holds
( E,f |= H 'or' H' iff ( E,f |= H or E,f |= H' ) )
let f be Function of VAR ,E; :: thesis: for H, H' being ZF-formula holds
( E,f |= H 'or' H' iff ( E,f |= H or E,f |= H' ) )
let H, H' be ZF-formula; :: thesis: ( E,f |= H 'or' H' iff ( E,f |= H or E,f |= H' ) )
( ( E,f |= 'not' (('not' H) '&' ('not' H')) implies not E,f |= ('not' H) '&' ('not' H') ) & ( not E,f |= ('not' H) '&' ('not' H') implies E,f |= 'not' (('not' H) '&' ('not' H')) ) & ( E,f |= ('not' H) '&' ('not' H') implies ( E,f |= 'not' H & E,f |= 'not' H' ) ) & ( E,f |= 'not' H & E,f |= 'not' H' implies E,f |= ('not' H) '&' ('not' H') ) & ( E,f |= 'not' H implies not E,f |= H ) & ( not E,f |= H implies E,f |= 'not' H ) & ( E,f |= 'not' H' implies not E,f |= H' ) & ( not E,f |= H' implies E,f |= 'not' H' ) ) by Th14, Th15;
hence ( E,f |= H 'or' H' iff ( E,f |= H or E,f |= H' ) ) ; :: thesis: verum