let d be non zero 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 x9 being object holds
( x9 in cell (x,x) iff x9 = x )
proof
let x9 be object ; :: thesis: ( x9 in cell (x,x) iff x9 = x )
thus ( x9 in cell (x,x) implies x9 = x ) :: thesis: ( x9 = x implies x9 in cell (x,x) )
proof
assume A1: x9 in cell (x,x) ; :: thesis: x9 = x
then reconsider x = x, x9 = x9 as Function of (Seg d),REAL by Def3;
now :: thesis: for i being Element of Seg d holds x9 . i = x . i
let i be Element of Seg d; :: thesis: x9 . i = x . i
A2: for i being Element of Seg d holds x . i <= x . i ;
then A3: x . i <= x9 . i by A1, Th21;
x9 . i <= x . i by A1, A2, Th21;
hence x9 . i = x . i by A3, XXREAL_0:1; :: thesis: verum
end;
hence x9 = x by FUNCT_2:63; :: thesis: verum
end;
thus ( x9 = x implies x9 in cell (x,x) ) by Th23; :: thesis: verum
end;
hence cell (x,x) = {x} by TARSKI:def 1; :: thesis: verum