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 )
hereby :: thesis: ( M |=0 F \/ G implies ( 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
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;
end;
assume A2: M |=0 F \/ G ; :: thesis: ( M |=0 F & M |=0 G )
thus M |=0 F :: thesis: M |=0 G
proof
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;
let A be Element of LTLB_WFF ; :: according to LTLAXIO5:def 2 :: thesis: ( A in G implies M |=0 A )
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