let a, b be natural Number ; :: thesis: ( a <= b iff Seg a c= Seg b )
thus ( a <= b implies Seg a c= Seg b ) :: thesis: ( Seg a c= Seg b implies a <= b )
proof
assume A1: a <= b ; :: thesis: Seg a c= Seg b
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg a or x in Seg b )
assume x in Seg a ; :: thesis: x in Seg b
then consider c being Nat such that
A3: ( x = c & 1 <= c & c <= a ) ;
c <= b by A1, A3, XXREAL_0:2;
hence x in Seg b by A3; :: thesis: verum
end;
assume A4: Seg a c= Seg b ; :: thesis: a <= b
now :: thesis: ( a <> 0 implies a <= b )
assume a <> 0 ; :: thesis: a <= b
then a in Seg a by Th3;
hence a <= b by A4, Th1; :: thesis: verum
end;
hence a <= b ; :: thesis: verum