let F, G be ext-real-membered set ; :: thesis: -- (F /\ G) = (-- F) /\ (-- G)
let i be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not i in -- (F /\ G) or i in (-- F) /\ (-- G) ) & ( not i in (-- F) /\ (-- G) or i in -- (F /\ G) ) )
hereby :: thesis: ( not i in (-- F) /\ (-- G) or i in -- (F /\ G) )
assume i in -- (F /\ G) ; :: thesis: i in (-- F) /\ (-- G)
then A1: - i in F /\ G by Th2;
then - i in G by XBOOLE_0:def 4;
then A2: i in -- G by Th2;
- i in F by A1, XBOOLE_0:def 4;
then i in -- F by Th2;
hence i in (-- F) /\ (-- G) by A2, XBOOLE_0:def 4; :: thesis: verum
end;
assume A3: i in (-- F) /\ (-- G) ; :: thesis: i in -- (F /\ G)
then i in -- G by XBOOLE_0:def 4;
then A4: - i in G by Th2;
i in -- F by A3, XBOOLE_0:def 4;
then - i in F by Th2;
then - i in F /\ G by A4, XBOOLE_0:def 4;
hence i in -- (F /\ G) by Th2; :: thesis: verum