let d be non zero Element of NAT ; :: thesis: for x being Element of REAL d holds cell x,x = {x}
let x be Element of REAL d; :: thesis: cell x,x = {x}
for x' being set holds
( x' in cell x,x iff x' = x )

proof

let x' be set ; :: thesis: ( x' in cell x,x iff x' = x )
thus ( x' in cell x,x implies x' = x ) :: thesis: ( x' = x implies x' in cell x,x )

proof

assume A1: x' in cell x,x ; :: thesis: x' = x
then reconsider x = x, x' = x' as Function of (Seg d),REAL by Def4;

now

let i be Element of Seg d; :: thesis: x' . i = x . i
for i being Element of Seg d holds x . i <= x . i ;
then ( x . i <= x' . i & x' . i <= x . i ) by A1, Th25;
hence x' . i = x . i by XXREAL_0:1; :: thesis: verum

end;

hence x' = x by FUNCT_2:113; :: thesis: verum

end;

thus ( x' = x implies x' in cell x,x ) by Th27; :: thesis: verum

end;

hence cell x,x = {x} by TARSKI:def 1; :: thesis: verum