let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( rng f = rng g implies rng (X_axis f) = rng (X_axis g) )
assume rng f = rng g ; :: thesis: rng (X_axis f) = rng (X_axis g)
hence ( rng (X_axis f) c= rng (X_axis g) & rng (X_axis g) c= rng (X_axis f) ) by Th20; :: according to XBOOLE_0:def 10 :: thesis: verum