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 )

thus M |= F :: thesis: M |= G

( ( 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 A2:
M |= F \/ G
; :: thesis: ( M |= F & M |= G )assume A1:
( M |= F & M |= G )
; :: thesis: M |= F \/ G

thus M |= F \/ G :: thesis: verum

end;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;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

thus M |= F :: thesis: M |= G

proof

thus
M |= G
:: thesis: verum
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;assume p in F ; :: thesis: M |= p

then p in F \/ G by XBOOLE_0:def 3;

hence M |= p by A2; :: 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;assume p in G ; :: thesis: M |= p

then p in F \/ G by XBOOLE_0:def 3;

hence M |= p by A2; :: thesis: verum