let n be Nat; :: thesis: for a, b, c being Element of REAL n st a < b & b < c holds
a < c
let a, b, c be Element of REAL n; :: thesis: ( a < b & b < c implies a < c )
assume that
A1: a < b and
A2: b < c ; :: thesis: a < c
for i being Nat st i in Seg n holds
a . i < c . i
proof
let i be Nat; :: thesis: ( i in Seg n implies a . i < c . i )
assume i in Seg n ; :: thesis: a . i < c . i
then ( a . i < b . i & b . i < c . i ) by A1, A2;
hence a . i < c . i by XXREAL_0:2; :: thesis: verum
end;
hence a < c ; :: thesis: verum