let U0 be Universal_Algebra; :: thesis: for u being object holds
( u in Sub U0 iff ex U1 being strict SubAlgebra of U0 st u = U1 )
let u be object ; :: thesis: ( u in Sub U0 iff ex U1 being strict SubAlgebra of U0 st u = U1 )
thus ( u in Sub U0 implies ex U1 being strict SubAlgebra of U0 st u = U1 ) :: thesis: ( ex U1 being strict SubAlgebra of U0 st u = U1 implies u in Sub U0 )
proof
assume u in Sub U0 ; :: thesis: ex U1 being strict SubAlgebra of U0 st u = U1
then u is strict SubAlgebra of U0 by UNIALG_2:def 14;
hence ex U1 being strict SubAlgebra of U0 st u = U1 ; :: thesis: verum
end;
thus ( ex U1 being strict SubAlgebra of U0 st u = U1 implies u in Sub U0 ) by UNIALG_2:def 14; :: thesis: verum