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 ;
[x,x] in the InternalRel of G1 \/ the InternalRel of G2 by A5, XBOOLE_0:def 3;
then A6: [x,x] in the InternalRel of G by A2, NECKLA_2:def 2;
x in the carrier of G1 \/ the carrier of G2 by A4, XBOOLE_0:def 3;
then x in the carrier of G by A2, NECKLA_2:def 2;
hence contradiction by A6, NECKLACE:def 5; :: 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 ;
[x,x] in the InternalRel of G1 \/ the InternalRel of G2 by A8, XBOOLE_0:def 3;
then A9: [x,x] in the InternalRel of G by A2, NECKLA_2:def 2;
x in the carrier of G1 \/ the carrier of G2 by A7, XBOOLE_0:def 3;
then x in the carrier of G by A2, NECKLA_2:def 2;
hence contradiction by A9, NECKLACE:def 5; :: 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 ;
[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 A14: [x,x] in the InternalRel of G by A10, NECKLA_2:def 3;
x in the carrier of G1 \/ the carrier of G2 by A12, XBOOLE_0:def 3;
then x in the carrier of G by A10, NECKLA_2:def 3;
hence contradiction by A14, NECKLACE:def 5; :: 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 ;
[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 A17: [x,x] in the InternalRel of G by A10, NECKLA_2:def 3;
x in the carrier of G1 \/ the carrier of G2 by A15, XBOOLE_0:def 3;
then x in the carrier of G by A10, NECKLA_2:def 3;
hence contradiction by A17, NECKLACE:def 5; :: thesis: verum
end;
end;
end;
end;
end;