set L = { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;
now :: thesis: for x being object st x in { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } holds
x in bool IndexedREAL
let x be object ; :: thesis: ( x in { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } implies x in bool IndexedREAL )
assume x in { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ; :: thesis: x in bool IndexedREAL
then consider p being Element of BinFinTrees IndexedREAL such that
A1: ( Leaves p = x & p in X ) ;
thus x in bool IndexedREAL by A1; :: thesis: verum
end;
hence { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } is Subset of (bool IndexedREAL) by TARSKI:def 3; :: thesis: verum