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