let FMT be non empty FMT_Space_Str ; :: thesis: ex S being RelStr st
for x being Element of FMT holds U_FMT x is Subset of S
set S = BoolePoset the carrier of FMT;
take BoolePoset the carrier of FMT ; :: thesis: for x being Element of FMT holds U_FMT x is Subset of (BoolePoset the carrier of FMT)
thus for x being Element of FMT holds U_FMT x is Subset of (BoolePoset the carrier of FMT) by WAYBEL_7:2; :: thesis: verum