let R be non empty finite negative_alliance RelStr ; :: thesis: for X being Subset of R holds UAp ((UAp X) `) c= (UAp X) `
let X be Subset of R; :: thesis: UAp ((UAp X) `) c= (UAp X) `
defpred S₁[ Subset of R] means UAp ((UAp $1) `) c= (UAp $1) ` ;
{} R = {} ;
then A1: S₁[ {} the carrier of R] ;
A2: for B being Subset of R
for b being Element of R st S₁[B] & not b in B holds
S₁[B \/ {b}]

proof

let B be Subset of R; :: thesis: for b being Element of R st S₁[B] & not b in B holds
S₁[B \/ {b}]
let b be Element of R; :: thesis: ( S₁[B] & not b in B implies S₁[B \/ {b}] )
assume z1: ( S₁[B] & not b in B ) ; :: thesis: S₁[B \/ {b}]
reconsider Bb = B \/ {b} as Subset of R ;
UAp ((UAp Bb) `) = UAp (((UAp B) \/ (UAp {b})) `) by ROUGHS_2:13
.= UAp (((UAp B) `) /\ ((UAp {b}) `)) by XBOOLE_1:53 ;
then Z2: UAp ((UAp Bb) `) c= (UAp ((UAp B) `)) /\ (UAp ((UAp {b}) `)) by UApCon;
(UAp ((UAp B) `)) /\ (UAp ((UAp {b}) `)) c= ((UAp B) `) /\ (UAp ((UAp {b}) `)) by z1, XBOOLE_1:26;
then Z3: UAp ((UAp Bb) `) c= ((UAp B) `) /\ (UAp ((UAp {b}) `)) by Z2, XBOOLE_1:1;
(UAp R) . (((UAp R) . {b}) `) c= ((UAp R) . {b}) ` by Prop137H;
then (UAp R) . (((UAp R) . {b}) `) c= (UAp {b}) ` by ROUGHS_2:def 11;
then (UAp R) . ((UAp {b}) `) c= (UAp {b}) ` by ROUGHS_2:def 11;
then UAp ((UAp {b}) `) c= (UAp {b}) ` by ROUGHS_2:def 11;
then z4: ((UAp B) `) /\ (UAp ((UAp {b}) `)) c= ((UAp B) `) /\ ((UAp {b}) `) by XBOOLE_1:26;
((UAp B) `) /\ ((UAp {b}) `) = ((UAp B) \/ (UAp {b})) ` by XBOOLE_1:53
.= (UAp Bb) ` by ROUGHS_2:13 ;
hence S₁[B \/ {b}] by z4, Z3, XBOOLE_1:1; :: thesis: verum

end;

for B being Subset of R holds S₁[B] from ROUGHS_3:sch 1(A1, A2);
hence UAp ((UAp X) `) c= (UAp X) ` ; :: thesis: verum