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 )

( 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;

end;

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

end;thus contradiction :: thesis: verum

proof
end;

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

end;

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;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

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;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

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

end;thus contradiction :: thesis: verum

proof
end;

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

end;

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;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

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;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