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 (BASSModel (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 (BASSModel (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 (BASSModel (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 (BASSModel (R,BASSIGN)) holds
( s |= f '&' g iff ( s |= f & s |= g ) )
let f, g be Assign of (BASSModel (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;
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; :: 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;
(Fid (f,S)) . s = TRUE by A5;
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 ; :: thesis: verum

end;

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