let S be non empty set ; 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 '&' g iff ( t |= f & t |= g ) )
let BASSIGN be 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 '&' g iff ( t |= f & t |= g ) )
let t be Element of Inf_seq S; for f, g being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= f '&' g iff ( t |= f & t |= g ) )
let f, g be Assign of (Inf_seqModel (S,BASSIGN)); ( t |= f '&' g iff ( t |= f & t |= g ) )
set S1 = Inf_seq S;
A1:
f '&' g = And_0 (f,g,S)
by Def50;
thus
( t |= f '&' g implies ( t |= f & t |= g ) )
( t |= f & t |= g implies t |= f '&' g )proof
assume
t |= f '&' g
;
( t |= f & t |= g )
then
(Fid ((And_0 (f,g,S)),(Inf_seq S))) . t = TRUE
by A1;
then A2:
(Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE
by Def49;
then
Castboolean ((Fid (g,(Inf_seq S))) . t) = TRUE
by XBOOLEAN:101;
then A3:
(Fid (g,(Inf_seq S))) . t = TRUE
by MODELC_1:def 4;
Castboolean ((Fid (f,(Inf_seq S))) . t) = TRUE
by A2, XBOOLEAN:101;
then
(Fid (f,(Inf_seq S))) . t = TRUE
by MODELC_1:def 4;
hence
(
t |= f &
t |= g )
by A3;
verum
end;
assume
( t |= f & t |= g )
; t |= f '&' g
then
( (Fid (f,(Inf_seq S))) . t = TRUE & (Fid (g,(Inf_seq S))) . t = TRUE )
;
then
(Castboolean ((Fid (f,(Inf_seq S))) . t)) '&' (Castboolean ((Fid (g,(Inf_seq S))) . t)) = TRUE
by MODELC_1:def 4;
then
(Fid ((f '&' g),(Inf_seq S))) . t = TRUE
by A1, Def49;
hence
t |= f '&' g
; verum