let A, B be complex-membered set ; :: thesis: -- (A /\ B) = (-- A) /\ (-- B)
let z be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not z in -- (A /\ B) or z in (-- A) /\ (-- B) ) & ( not z in (-- A) /\ (-- B) or z in -- (A /\ B) ) )
hereby :: thesis: ( not z in (-- A) /\ (-- B) or z in -- (A /\ B) )
assume z in -- (A /\ B) ; :: thesis: z in (-- A) /\ (-- B)
then A1: - z in A /\ B by Th12;
then - z in B by XBOOLE_0:def 4;
then A2: z in -- B by Th12;
- z in A by A1, XBOOLE_0:def 4;
then z in -- A by Th12;
hence z in (-- A) /\ (-- B) by A2, XBOOLE_0:def 4; :: thesis: verum
end;
assume A3: z in (-- A) /\ (-- B) ; :: thesis: z in -- (A /\ B)
then z in -- B by XBOOLE_0:def 4;
then A4: - z in B by Th12;
z in -- A by A3, XBOOLE_0:def 4;
then - z in A by Th12;
then - z in A /\ B by A4, XBOOLE_0:def 4;
hence z in -- (A /\ B) by Th12; :: thesis: verum