consider F2 being proper Filter of (BoolePoset the carrier of T) such that
A1: F = F2 by Th37;
thus F is proper Filter of (BoolePoset ([#] T)) by A1; :: thesis: verum