let U1, U2 be Universal_Algebra; :: thesis: ( UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) implies for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 & S1 is opers_closed holds
S2 is opers_closed )
assume A1: UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) ; :: thesis: for S1 being Subset of U1
for S2 being Subset of U2 st S1 = S2 & S1 is opers_closed holds
S2 is opers_closed
let S1 be Subset of U1; :: thesis: for S2 being Subset of U2 st S1 = S2 & S1 is opers_closed holds
S2 is opers_closed
let S2 be Subset of U2; :: thesis: ( S1 = S2 & S1 is opers_closed implies S2 is opers_closed )
assume A2: S1 = S2 ; :: thesis: ( not S1 is opers_closed or S2 is opers_closed )
assume A3: for o being operation of U1 holds S1 is_closed_on o ; :: according to UNIALG_2:def 4 :: thesis: S2 is opers_closed
let o be operation of U2; :: according to UNIALG_2:def 4 :: thesis: S2 is_closed_on o
reconsider o1 = o as operation of U1 by A1;
S1 is_closed_on o1 by A3;
hence S2 is_closed_on o by A2; :: thesis: verum