let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0
let OU0 be OSAlgebra of S1; :: thesis: OSSub OU0 c= MSSub OU0
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OSSub OU0 or x in MSSub OU0 )
assume x in OSSub OU0 ; :: thesis: x in MSSub OU0
then x is strict MSSubAlgebra of OU0 by Def14;
hence x in MSSub OU0 by MSUALG_2:def 19; :: thesis: verum