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 )

( 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

thus
( ex U1 being strict SubAlgebra of U0 st u = U1 implies u in Sub U0 )
by UNIALG_2:def 14; :: thesis: verum
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;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