let F, G be Subset of LTLB_WFF; :: thesis: for M being LTLModel holds

( ( M |=0 F & M |=0 G ) iff M |=0 F \/ G )

let M be LTLModel; :: thesis: ( ( M |=0 F & M |=0 G ) iff M |=0 F \/ G )

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

assume A in G ; :: thesis: M |=0 A

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

hence M |=0 A by A2; :: thesis: verum

( ( M |=0 F & M |=0 G ) iff M |=0 F \/ G )

let M be LTLModel; :: thesis: ( ( M |=0 F & M |=0 G ) iff M |=0 F \/ G )

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

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

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

end;thus M |=0 F \/ G :: thesis: verum

proof

let A be Element of LTLB_WFF ; :: according to LTLAXIO5:def 2 :: thesis: ( A in F \/ G implies M |=0 A )

assume A in F \/ G ; :: thesis: M |=0 A

then ( A in F or A in G ) by XBOOLE_0:def 3;

hence M |=0 A by A1; :: thesis: verum

end;assume A in F \/ G ; :: thesis: M |=0 A

then ( A in F or A in G ) by XBOOLE_0:def 3;

hence M |=0 A by A1; :: thesis: verum

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

proof

let A be Element of LTLB_WFF ; :: according to LTLAXIO5:def 2 :: thesis: ( A in G implies M |=0 A )
let A be Element of LTLB_WFF ; :: according to LTLAXIO5:def 2 :: thesis: ( A in F implies M |=0 A )

assume A in F ; :: thesis: M |=0 A

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

hence M |=0 A by A2; :: thesis: verum

end;assume A in F ; :: thesis: M |=0 A

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

hence M |=0 A by A2; :: thesis: verum

assume A in G ; :: thesis: M |=0 A

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

hence M |=0 A by A2; :: thesis: verum