let A be Universal_Algebra; for B, C being Subset of A st C is opers_closed & B c= C holds
union { (B |^ n) where n is Element of NAT : verum } c= C
let B, C be Subset of A; ( C is opers_closed & B c= C implies union { (B |^ n) where n is Element of NAT : verum } c= C )
assume A1:
C is opers_closed
; ( not B c= C or union { (B |^ n) where n is Element of NAT : verum } c= C )
assume A2:
B c= C
; union { (B |^ n) where n is Element of NAT : verum } c= C
let z be object ; TARSKI:def 3 ( z nin union { (B |^ n) where n is Element of NAT : verum } or not z nin C )
assume
z in union { (B |^ n) where n is Element of NAT : verum }
; not z nin C
then consider Y being set such that
A3:
z in Y
and
A4:
Y in { (B |^ n) where n is Element of NAT : verum }
by TARSKI:def 4;
consider n being Element of NAT such that
A5:
Y = B |^ n
by A4;
defpred S1[ Nat] means B |^ $1 c= C;
A6:
S1[ 0 ]
by A2, Th18;
A7:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A8:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
let x be
object ;
TARSKI:def 3 ( x nin B |^ (n + 1) or not x nin C )
assume that A9:
x in B |^ (n + 1)
and A10:
x nin C
;
contradiction
x in (B |^ n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B |^ n ) }
by A9, Th19;
then
(
x in B |^ n or
x in { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B |^ n ) } )
by XBOOLE_0:def 3;
then consider o being
Element of
dom the
charact of
A,
p being
Element of the
carrier of
A * such that A11:
x = (Den (o,A)) . p
and A12:
p in dom (Den (o,A))
and A13:
rng p c= B |^ n
by A8, A10;
rng p c= C
by A8, A13, XBOOLE_1:1;
then reconsider p =
p as
FinSequence of
C by FINSEQ_1:def 4;
reconsider oo =
Den (
o,
A) as
Element of
Operations A ;
A14:
len p = arity oo
by A12, MARGREL1:def 25;
C is_closed_on oo
by A1;
hence
contradiction
by A10, A11, A14;
verum
end; end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A7);
then
S1[n]
;
hence
not z nin C
by A3, A5; verum