( S1 c= Fml & S2 c= Fml ) by Def4;
hence S1 \/ S2 is Formula-finset of Fml by Def4, XBOOLE_1:8; :: thesis: verum