let A be Universal_Algebra; :: thesis: for B being Subset of A holds B |^ 0 = B
let B be Subset of A; :: thesis: B |^ 0 = B
ex F being sequence of (bool the carrier of A) st
( B |^ 0 = F . 0 & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . 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= F . n ) } ) ) by Def8;
hence B |^ 0 = B ; :: thesis: verum