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

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