let X be finite binary DecoratedTree of IndexedREAL ; :: thesis: LeavesSet {X} = {(Leaves X)}
for x being object holds
( x in LeavesSet {X} iff x in {(Leaves X)} )
proof
let x be object ; :: thesis: ( x in LeavesSet {X} iff x in {(Leaves X)} )
hereby :: thesis: ( x in {(Leaves X)} implies x in LeavesSet {X} )
assume x in LeavesSet {X} ; :: thesis: x in {(Leaves X)}
then consider p being Element of BinFinTrees IndexedREAL such that
A1: ( x = Leaves p & p in {X} ) ;
p = X by A1, TARSKI:def 1;
hence x in {(Leaves X)} by TARSKI:def 1, A1; :: thesis: verum
end;
assume x in {(Leaves X)} ; :: thesis: x in LeavesSet {X}
then A2: x = Leaves X by TARSKI:def 1;
( dom X is finite & dom X is binary ) by BINTREE1:def 3;
then reconsider p = X as Element of BinFinTrees IndexedREAL by Def2;
p in {X} by TARSKI:def 1;
hence x in LeavesSet {X} by A2; :: thesis: verum
end;
hence LeavesSet {X} = {(Leaves X)} by TARSKI:2; :: thesis: verum