let x be Element of (RealPoset [.0,1.]); :: thesis: x is Real
( x in the carrier of (RealPoset [.0,1.]) & the carrier of (RealPoset [.0,1.]) = [.0,1.] ) by Def3;
hence x is Real ; :: thesis: verum