let F, G be Subset of [:(LTLB_WFF **),(LTLB_WFF **):]; :: thesis: (F \/ G) ^ = (F ^) \/ (G ^)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (F ^) \/ (G ^) c= (F \/ G) ^

let x be object ; :: thesis: ( x in (F \/ G) ^ implies x in (F ^) \/ (G ^) )
assume x in (F \/ G) ^ ; :: thesis: x in (F ^) \/ (G ^)
then consider P being PNPair such that
A1: x = P ^ and
A2: P in F \/ G ;
( P in F or P in G ) by A2, XBOOLE_0:def 3;
then ( x in F ^ or x in G ^ ) by A1;
hence x in (F ^) \/ (G ^) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (F ^) \/ (G ^) or x in (F \/ G) ^ )
assume A3: x in (F ^) \/ (G ^) ; :: thesis: x in (F \/ G) ^

per cases ( x in F ^ or x in G ^ ) by A3, XBOOLE_0:def 3;

suppose x in F ^ ; :: thesis: x in (F \/ G) ^

then consider P being PNPair such that
A4: x = P ^ and
A5: P in F ;
P in F \/ G by A5, XBOOLE_0:def 3;
hence x in (F \/ G) ^ by A4; :: thesis: verum

end;

suppose x in G ^ ; :: thesis: x in (F \/ G) ^

then consider P being PNPair such that
A6: x = P ^ and
A7: P in G ;
P in F \/ G by A7, XBOOLE_0:def 3;
hence x in (F \/ G) ^ by A6; :: thesis: verum

end;

end;