let G be irreflexive RelStr ; :: thesis: for G1, G2 being RelStr st ( G = union_of G1,G2 or G = sum_of G1,G2 ) holds
( G1 is irreflexive & G2 is irreflexive )
let G1, G2 be RelStr ; :: thesis: ( ( G = union_of G1,G2 or G = sum_of G1,G2 ) implies ( G1 is irreflexive & G2 is irreflexive ) )
assume A1: ( G = union_of G1,G2 or G = sum_of G1,G2 ) ; :: thesis: ( G1 is irreflexive & G2 is irreflexive )

per cases ( G = union_of G1,G2 or G = sum_of G1,G2 ) by A1;

suppose A2: G = union_of G1,G2 ; :: thesis: ( G1 is irreflexive & G2 is irreflexive )

assume A3: ( not G1 is irreflexive or not G2 is irreflexive ) ; :: thesis: contradiction
thus contradiction :: thesis: verum

proof

per cases ( not G1 is irreflexive or not G2 is irreflexive ) by A3;

suppose not G1 is irreflexive ; :: thesis: contradiction

then consider x being set such that
A4: x in the carrier of G1 and
A5: [x,x] in the InternalRel of G1 by NECKLACE:def 6;
x in the carrier of G1 \/ the carrier of G2 by A4, XBOOLE_0:def 3;
then A6: x in the carrier of G by A2, NECKLA_2:def 2;
[x,x] in the InternalRel of G1 \/ the InternalRel of G2 by A5, XBOOLE_0:def 3;
then [x,x] in the InternalRel of G by A2, NECKLA_2:def 2;
hence contradiction by A6, NECKLACE:def 6; :: thesis: verum

end;

suppose not G2 is irreflexive ; :: thesis: contradiction

then consider x being set such that
A7: x in the carrier of G2 and
A8: [x,x] in the InternalRel of G2 by NECKLACE:def 6;
x in the carrier of G1 \/ the carrier of G2 by A7, XBOOLE_0:def 3;
then A9: x in the carrier of G by A2, NECKLA_2:def 2;
[x,x] in the InternalRel of G1 \/ the InternalRel of G2 by A8, XBOOLE_0:def 3;
then [x,x] in the InternalRel of G by A2, NECKLA_2:def 2;
hence contradiction by A9, NECKLACE:def 6; :: thesis: verum

end;

end;

end;

end;

suppose A10: G = sum_of G1,G2 ; :: thesis: ( G1 is irreflexive & G2 is irreflexive )

assume A11: ( not G1 is irreflexive or not G2 is irreflexive ) ; :: thesis: contradiction
thus contradiction :: thesis: verum

proof

per cases ( not G1 is irreflexive or not G2 is irreflexive ) by A11;

suppose not G1 is irreflexive ; :: thesis: contradiction

then consider x being set such that
A12: x in the carrier of G1 and
A13: [x,x] in the InternalRel of G1 by NECKLACE:def 6;
x in the carrier of G1 \/ the carrier of G2 by A12, XBOOLE_0:def 3;
then A14: x in the carrier of G by A10, NECKLA_2:def 3;
[x,x] in the InternalRel of G1 \/ the InternalRel of G2 by A13, XBOOLE_0:def 3;
then [x,x] in (the InternalRel of G1 \/ the InternalRel of G2) \/ [:the carrier of G1,the carrier of G2:] by XBOOLE_0:def 3;
then [x,x] in ((the InternalRel of G1 \/ the InternalRel of G2) \/ [:the carrier of G1,the carrier of G2:]) \/ [:the carrier of G2,the carrier of G1:] by XBOOLE_0:def 3;
then [x,x] in the InternalRel of G by A10, NECKLA_2:def 3;
hence contradiction by A14, NECKLACE:def 6; :: thesis: verum

end;

suppose not G2 is irreflexive ; :: thesis: contradiction

then consider x being set such that
A15: x in the carrier of G2 and
A16: [x,x] in the InternalRel of G2 by NECKLACE:def 6;
x in the carrier of G1 \/ the carrier of G2 by A15, XBOOLE_0:def 3;
then A17: x in the carrier of G by A10, NECKLA_2:def 3;
[x,x] in the InternalRel of G1 \/ the InternalRel of G2 by A16, XBOOLE_0:def 3;
then [x,x] in (the InternalRel of G1 \/ the InternalRel of G2) \/ [:the carrier of G1,the carrier of G2:] by XBOOLE_0:def 3;
then [x,x] in ((the InternalRel of G1 \/ the InternalRel of G2) \/ [:the carrier of G1,the carrier of G2:]) \/ [:the carrier of G2,the carrier of G1:] by XBOOLE_0:def 3;
then [x,x] in the InternalRel of G by A10, NECKLA_2:def 3;
hence contradiction by A17, NECKLACE:def 6; :: thesis: verum

end;

end;

end;

end;

end;