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 set ; :: 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
A2: ( p1 in field (R \/ S) & p2 in field (R \/ S) & 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 ( [p1,p2] in R & [p2,p3] in R ) by A1, A3, A4, A5, Lm1;
then [p1,p3] in R by RELAT_2:48;
hence [^,^] in R \/ S by XBOOLE_0:def 3; :: thesis: verum

end;

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

then p2 in S1 by A1, A4, Lm1;
then ( [p1,p2] in S & [p2,p3] in S ) by A1, A3, A4, A6, Lm1;
then [p1,p3] in S by RELAT_2:48;
hence [^,^] in R \/ S by XBOOLE_0:def 3; :: thesis: verum

end;

end;