let R1, S1 be set ; for R being transitive Relation of R1
for S being transitive Relation of S1 st R1 misses S1 holds
R \/ S is transitive
let R be transitive Relation of R1; for S being transitive Relation of S1 st R1 misses S1 holds
R \/ S is transitive
let S be transitive Relation of S1; ( R1 misses S1 implies R \/ S is transitive )
assume A1:
R1 misses S1
; R \/ S is transitive
let p1, p2, p3 be object ; RELAT_2:def 8,RELAT_2:def 16 ( not p1 in field (R \/ S) or not p2 in field (R \/ S) or not p3 in field (R \/ S) or not [^,^] in R \/ S or not [^,^] in R \/ S or [^,^] in R \/ S )
set RS = R \/ S;
set D = field (R \/ S);
assume that
p1 in field (R \/ S)
and
p2 in field (R \/ S)
and
A2:
p3 in field (R \/ S)
and
A3:
[p1,p2] in R \/ S
and
A4:
[p2,p3] in R \/ S
; [^,^] in R \/ S
per cases
( p3 in R1 or p3 in S1 )
by A2, XBOOLE_0:def 3;
suppose A5:
p3 in R1
;
[^,^] in R \/ Sthen
p2 in R1
by A1, A4, Lm1;
then A6:
[p1,p2] in R
by A1, A3, Lm1;
[p2,p3] in R
by A1, A4, A5, Lm1;
then
[p1,p3] in R
by A6, RELAT_2:31;
hence
[^,^] in R \/ S
by XBOOLE_0:def 3;
verum end; suppose A7:
p3 in S1
;
[^,^] in R \/ Sthen
p2 in S1
by A1, A4, Lm1;
then A8:
[p1,p2] in S
by A1, A3, Lm1;
[p2,p3] in S
by A1, A4, A7, Lm1;
then
[p1,p3] in S
by A8, RELAT_2:31;
hence
[^,^] in R \/ S
by XBOOLE_0:def 3;
verum end;