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 (LTLModel S,BASSIGN) holds
( t |= f '&' g iff ( t |= f & 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 (LTLModel S,BASSIGN) holds
( t |= f '&' g iff ( t |= f & t |= g ) )
let t be Element of Inf_seq S; :: thesis: for f, g being Assign of (LTLModel S,BASSIGN) holds
( t |= f '&' g iff ( t |= f & t |= g ) )
let f, g be Assign of (LTLModel S,BASSIGN); :: thesis: ( t |= f '&' g iff ( t |= f & t |= g ) )
set V = LTLModel S,BASSIGN;
set S1 = Inf_seq S;
A1: f '&' g = And_0 f,g,S by Def52;
thus ( t |= f '&' g implies ( t |= f & t |= g ) ) :: thesis: ( t |= f & t |= g implies t |= f '&' g )

proof

assume t |= f '&' g ; :: thesis: ( t |= f & t |= g )
then (Fid (And_0 f,g,S),(Inf_seq S)) . t = TRUE by A1, Def59;
then A2: (Castboolean ((Fid f,(Inf_seq S)) . t)) '&' (Castboolean ((Fid g,(Inf_seq S)) . t)) = TRUE by Def51;
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, Def59; :: thesis: verum

end;

assume ( t |= f & t |= g ) ; :: thesis: t |= f '&' g
then ( (Fid f,(Inf_seq S)) . t = TRUE & (Fid g,(Inf_seq S)) . t = TRUE ) by Def59;
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, Def51;
hence t |= f '&' g by Def59; :: thesis: verum