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 )

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

thus
( u in H implies u in (Carr U0) . H )
:: thesis: verum
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;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

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;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