let S be non empty set ; :: thesis: 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 (CTLModel R,BASSIGN) holds
( s |= f '&' g iff ( s |= f & s |= g ) )
let R be total Relation of S,S; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN) holds
( s |= f '&' g iff ( s |= f & s |= g ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN) holds
( s |= f '&' g iff ( s |= f & s |= g ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (CTLModel R,BASSIGN) holds
( s |= f '&' g iff ( s |= f & s |= g ) )
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: ( s |= f '&' g iff ( s |= f & s |= g ) )
A1: f '&' g = And_0 f,g,S by Def51;
A2: ( s |= f '&' g implies ( s |= f & s |= g ) )

proof

assume s |= f '&' g ; :: thesis: ( s |= f & s |= g )
then (Fid (And_0 f,g,S),S) . s = TRUE by A1, Def59;
then A3: (Castboolean ((Fid f,S) . s)) '&' (Castboolean ((Fid g,S) . s)) = TRUE by Def50;
then Castboolean ((Fid g,S) . s) = TRUE by XBOOLEAN:101;
then A4: (Fid g,S) . s = TRUE by Def4;
Castboolean ((Fid f,S) . s) = TRUE by A3, XBOOLEAN:101;
then (Fid f,S) . s = TRUE by Def4;
hence ( s |= f & s |= g ) by A4, Def59; :: thesis: verum

end;

( s |= f & s |= g implies s |= f '&' g )

proof

assume that
A5: s |= f and
A6: s |= g ; :: thesis: s |= f '&' g
A7: (Fid g,S) . s = TRUE by A6, Def59;
(Fid f,S) . s = TRUE by A5, Def59;
then (Castboolean ((Fid f,S) . s)) '&' (Castboolean ((Fid g,S) . s)) = TRUE by A7, Def4;
then (Fid (f '&' g),S) . s = TRUE by A1, Def50;
hence s |= f '&' g by Def59; :: thesis: verum

end;

hence ( s |= f '&' g iff ( s |= f & s |= g ) ) by A2; :: thesis: verum