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 being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= 'not' f iff t |/= f )
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); :: thesis: for t being Element of Inf_seq S
for f being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= 'not' f iff t |/= f )
let t be Element of Inf_seq S; :: thesis: for f being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= 'not' f iff t |/= f )
let f be Assign of (Inf_seqModel (S,BASSIGN)); :: thesis: ( t |= 'not' f iff t |/= f )
set S1 = Inf_seq S;
A1: 'not' f = Not_0 (f,S) by Def49;
thus ( t |= 'not' f implies t |/= f ) :: thesis: ( t |/= f implies t |= 'not' f )

proof

assume t |= 'not' f ; :: thesis: t |/= f
then (Fid (('not' f),(Inf_seq S))) . t = TRUE by Def61;
then 'not' (Castboolean ((Fid (f,(Inf_seq S))) . t)) = TRUE by A1, Def48;
then (Fid (f,(Inf_seq S))) . t = FALSE by MODELC_1:def 4;
hence t |/= f by Def61; :: thesis: verum

end;

assume t |/= f ; :: thesis: t |= 'not' f
then not (Fid (f,(Inf_seq S))) . t = TRUE by Def61;
then not Castboolean ((Fid (f,(Inf_seq S))) . t) = TRUE by MODELC_1:def 4;
then Castboolean ((Fid (f,(Inf_seq S))) . t) = FALSE by XBOOLEAN:def 3;
then 'not' (Castboolean ((Fid (f,(Inf_seq S))) . t)) = TRUE ;
then (Fid (('not' f),(Inf_seq S))) . t = TRUE by A1, Def48;
hence t |= 'not' f by Def61; :: thesis: verum