let R1, S1 be set ; :: thesis: 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; :: thesis: for S being transitive Relation of S1 st R1 misses S1 holds
R \/ S is transitive
let S be transitive Relation of S1; :: thesis: ( R1 misses S1 implies R \/ S is transitive )
assume A1: R1 misses S1 ; :: thesis: R \/ S is transitive
let p1, p2, p3 be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( 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 ; :: thesis: [^,^] in R \/ S

per cases ( p3 in R1 or p3 in S1 ) by A2, XBOOLE_0:def 3;

suppose A5: p3 in R1 ; :: thesis: [^,^] in R \/ S

then 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; :: thesis: verum

end;

suppose A7: p3 in S1 ; :: thesis: [^,^] in R \/ S

then 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; :: thesis: verum

end;

end;