let X be non empty addLoopStr ; :: thesis: for M, N being Subset of X holds { (x + N) where x is Point of X : x in M } is Subset-Family of X
let M, N be Subset of X; :: thesis: { (x + N) where x is Point of X : x in M } is Subset-Family of X
set F = { (u + N) where u is Point of X : u in M } ;
{ (u + N) where u is Point of X : u in M } c= bool the carrier of X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (u + N) where u is Point of X : u in M } or x in bool the carrier of X )
assume x in { (u + N) where u is Point of X : u in M } ; :: thesis: x in bool the carrier of X
then ex u being Point of X st
( x = u + N & u in M ) ;
hence x in bool the carrier of X ; :: thesis: verum

end;

hence { (x + N) where x is Point of X : x in M } is Subset-Family of X ; :: thesis: verum