let R be Relation of X; :: thesis: ( R is connected & R is total & R is transitive implies R is beta-transitive )
assume A1: ( R is connected & R is total & R is transitive ) ; :: thesis: R is beta-transitive
then field R = X by ORDERS_1:12;
then A2: R is_connected_in X by A1;
let x, y be Element of X; :: according to MMLQUER2:def 4 :: thesis: ( x,y nin R implies for z being Element of X st x,z in R holds
y,z in R )
assume A3: x,y nin R ; :: thesis: for z being Element of X st x,z in R holds
y,z in R
let z be Element of X; :: thesis: ( x,z in R implies y,z in R )
assume A4: [x,z] in R ; :: according to MMLQUERY:def 1 :: thesis: y,z in R
then x in X by ZFMISC_1:87;
then ( not x <> y or [x,y] in R or [y,x] in R ) by A2;
then ( ( x = y or y,x in R ) & x,z in R ) by A3, A4;
hence y,z in R by A1; :: thesis: verum