let U0 be Universal_Algebra; :: thesis: for H being strict SubAlgebra of U0
for u being Element of U0 holds
( u in (Carr U0) . H iff u in H )
let H be strict SubAlgebra of U0; :: thesis: for u being Element of U0 holds
( u in (Carr U0) . H iff u in H )
let u be Element of U0; :: thesis: ( u in (Carr U0) . H iff u in H )
thus ( u in (Carr U0) . H implies u in H ) :: thesis: ( u in H implies u in (Carr U0) . H )
proof
A1: H in Sub U0 by UNIALG_2:def 14;
assume u in (Carr U0) . H ; :: thesis: u in H
then u in the carrier of H by A1, Def4;
hence u in H by STRUCT_0:def 5; :: thesis: verum
end;
thus ( u in H implies u in (Carr U0) . H ) :: thesis: verum
proof
H in Sub U0 by UNIALG_2:def 14;
then A2: (Carr U0) . H = the carrier of H by Def4;
assume u in H ; :: thesis: u in (Carr U0) . H
hence u in (Carr U0) . H by A2, STRUCT_0:def 5; :: thesis: verum
end;