let A, B be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )
let n be Element of NAT ; :: thesis: for M being LTLModel holds
( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )
let M be LTLModel; :: thesis: ( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )

hereby :: thesis: ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 implies (SAT M) . [n,(A '&&' B)] = 1 )

assume (SAT M) . [n,(A '&&' B)] = 1 ; :: thesis: ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 )
then ((SAT M) . [n,(A => (B => TFALSUM))]) => ((SAT M) . [n,TFALSUM]) = 1 by Def11;
then ((SAT M) . [n,(A => (B => TFALSUM))]) => FALSE = 1 by Def11;
then ((SAT M) . [n,A]) => ((SAT M) . [n,(B => TFALSUM)]) = 0 by Def11;
then ((SAT M) . [n,A]) => (((SAT M) . [n,B]) => ((SAT M) . [n,TFALSUM])) = 0 by Def11;
then A1: ((SAT M) . [n,A]) => (((SAT M) . [n,B]) => FALSE) = 0 by Def11;
( (SAT M) . [n,A] = 0 or (SAT M) . [n,A] = 1 ) by XBOOLEAN:def 3;
hence ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) by A1; :: thesis: verum

end;

assume that
A2: (SAT M) . [n,A] = 1 and
A3: (SAT M) . [n,B] = 1 ; :: thesis: (SAT M) . [n,(A '&&' B)] = 1
((SAT M) . [n,B]) => ((SAT M) . [n,TFALSUM]) = 0 by A3, Def11;
then ((SAT M) . [n,A]) => ((SAT M) . [n,(B => TFALSUM)]) = 0 by A2, Def11;
then (SAT M) . [n,(A => (B => TFALSUM))] = 0 by Def11;
then ((SAT M) . [n,(A => (B => TFALSUM))]) => ((SAT M) . [n,TFALSUM]) = 1 ;
hence (SAT M) . [n,(A '&&' B)] = 1 by Def11; :: thesis: verum