let R be non empty finite negative_alliance RelStr ; :: thesis: for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `)
for X being Subset of R holds UAp ((UAp X) `) c= (UAp X) ` by Prop13H;
hence for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `) by Conv; :: thesis: verum