let F, G be Subset of LTLB_WFF; :: thesis: for M being LTLModel holds
( ( M |= F & M |= G ) iff M |= F \/ G )
let M be LTLModel; :: thesis: ( ( M |= F & M |= G ) iff M |= F \/ G )

hereby :: thesis: ( M |= F \/ G implies ( M |= F & M |= G ) )

assume A1: ( M |= F & M |= G ) ; :: thesis: M |= F \/ G
thus M |= F \/ G :: thesis: verum

proof

let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def 13 :: thesis: ( p in F \/ G implies M |= p )
assume p in F \/ G ; :: thesis: M |= p
then ( p in F or p in G ) by XBOOLE_0:def 3;
hence M |= p by A1; :: thesis: verum

end;

end;

assume A2: M |= F \/ G ; :: thesis: ( M |= F & M |= G )
thus M |= F :: thesis: M |= G

proof

let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def 13 :: thesis: ( p in F implies M |= p )
assume p in F ; :: thesis: M |= p
then p in F \/ G by XBOOLE_0:def 3;
hence M |= p by A2; :: thesis: verum

end;

thus M |= G :: thesis: verum

proof

let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def 13 :: thesis: ( p in G implies M |= p )
assume p in G ; :: thesis: M |= p
then p in F \/ G by XBOOLE_0:def 3;
hence M |= p by A2; :: thesis: verum

end;