let X be Tolerance_Space; :: thesis: RSLattice X is complete

let Y be Subset of (RSLattice X); :: according to VECTSP_8:def 6 :: thesis: ex b_{1} being Element of the carrier of (RSLattice X) st

( b_{1} is_less_than Y & ( for b_{2} being Element of the carrier of (RSLattice X) holds

( not b_{2} is_less_than Y or b_{2} [= b_{1} ) ) )

ex a being Element of (RSLattice X) st

( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )_{1} being Element of the carrier of (RSLattice X) st

( b_{1} is_less_than Y & ( for b_{2} being Element of the carrier of (RSLattice X) holds

( not b_{2} is_less_than Y or b_{2} [= b_{1} ) ) )
; :: thesis: verum

let Y be Subset of (RSLattice X); :: according to VECTSP_8:def 6 :: thesis: ex b

( b

( not b

ex a being Element of (RSLattice X) st

( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )

proof
end;

hence
ex bper cases
( Y is empty or not Y is empty )
;

end;

suppose A1:
Y is empty
; :: thesis: ex a being Element of (RSLattice X) st

( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )

( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )

take a = Top (RSLattice X); :: thesis: ( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )

for q being Element of (RSLattice X) st q in Y holds

a [= q by A1;

hence a is_less_than Y ; :: thesis: for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a

let b be Element of (RSLattice X); :: thesis: ( b is_less_than Y implies b [= a )

assume b is_less_than Y ; :: thesis: b [= a

thus b [= a by LATTICES:19; :: thesis: verum

end;b [= a ) )

for q being Element of (RSLattice X) st q in Y holds

a [= q by A1;

hence a is_less_than Y ; :: thesis: for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a

let b be Element of (RSLattice X); :: thesis: ( b is_less_than Y implies b [= a )

assume b is_less_than Y ; :: thesis: b [= a

thus b [= a by LATTICES:19; :: thesis: verum

suppose A2:
not Y is empty
; :: thesis: ex a being Element of (RSLattice X) st

( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )

( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )

set A1 = { (LAp a1) where a1 is RoughSet of X : a1 in Y } ;

set A2 = { (UAp a1) where a1 is RoughSet of X : a1 in Y } ;

set a9 = [(meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ),(meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } )];

consider f being object such that

A3: f in Y by A2;

Y is Subset of (RoughSets X) by Def23;

then reconsider f = f as RoughSet of X by A3, Def20;

A4: LAp f in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by A3;

then A5: { (LAp a1) where a1 is RoughSet of X : a1 in Y } <> {} ;

consider g being object such that

A6: g in Y by A2;

Y is Subset of (RoughSets X) by Def23;

then reconsider g = g as RoughSet of X by A6, Def20;

UAp g in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by A6;

then A7: { (UAp a1) where a1 is RoughSet of X : a1 in Y } <> {} ;

A8: meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } c= the carrier of X

a9 in RoughSets X by Def20;

then reconsider a = a9 as Element of (RSLattice X) by Def23;

take a ; :: thesis: ( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )

thus a is_less_than Y :: thesis: for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a

b [= a :: thesis: verum

end;set A2 = { (UAp a1) where a1 is RoughSet of X : a1 in Y } ;

set a9 = [(meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ),(meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } )];

consider f being object such that

A3: f in Y by A2;

Y is Subset of (RoughSets X) by Def23;

then reconsider f = f as RoughSet of X by A3, Def20;

A4: LAp f in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by A3;

then A5: { (LAp a1) where a1 is RoughSet of X : a1 in Y } <> {} ;

consider g being object such that

A6: g in Y by A2;

Y is Subset of (RoughSets X) by Def23;

then reconsider g = g as RoughSet of X by A6, Def20;

UAp g in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by A6;

then A7: { (UAp a1) where a1 is RoughSet of X : a1 in Y } <> {} ;

A8: meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } c= the carrier of X

proof

[(meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ),(meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } )] is RoughSet of X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } or x in the carrier of X )

assume x in meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: x in the carrier of X

then A9: for Z being set st Z in { (LAp a1) where a1 is RoughSet of X : a1 in Y } holds

x in Z by SETFAM_1:def 1;

consider c being set such that

A10: c in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by A4;

consider c9 being RoughSet of X such that

A11: ( c = LAp c9 & c9 in Y ) by A10;

A12: c in bool the carrier of X by A11;

x in c by A10, A9;

hence x in the carrier of X by A12; :: thesis: verum

end;assume x in meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: x in the carrier of X

then A9: for Z being set st Z in { (LAp a1) where a1 is RoughSet of X : a1 in Y } holds

x in Z by SETFAM_1:def 1;

consider c being set such that

A10: c in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by A4;

consider c9 being RoughSet of X such that

A11: ( c = LAp c9 & c9 in Y ) by A10;

A12: c in bool the carrier of X by A11;

x in c by A10, A9;

hence x in the carrier of X by A12; :: thesis: verum

proof

then reconsider a9 = [(meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ),(meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } )] as RoughSet of X ;
meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } c= the carrier of X

hence [(meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ),(meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } )] is RoughSet of X by Def13; :: thesis: verum

end;proof

then
[(meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ),(meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } )] in [:(bool the carrier of X),(bool the carrier of X):]
by A8, ZFMISC_1:87;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } or x in the carrier of X )

assume x in meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: x in the carrier of X

then A13: for Z being set st Z in { (UAp a1) where a1 is RoughSet of X : a1 in Y } holds

x in Z by SETFAM_1:def 1;

consider c being object such that

A14: c in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by A7, XBOOLE_0:def 1;

consider c9 being RoughSet of X such that

A15: ( c = UAp c9 & c9 in Y ) by A14;

reconsider c = c as set by TARSKI:1;

A16: c c= the carrier of X by A15;

x in c by A14, A13;

hence x in the carrier of X by A16; :: thesis: verum

end;assume x in meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: x in the carrier of X

then A13: for Z being set st Z in { (UAp a1) where a1 is RoughSet of X : a1 in Y } holds

x in Z by SETFAM_1:def 1;

consider c being object such that

A14: c in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by A7, XBOOLE_0:def 1;

consider c9 being RoughSet of X such that

A15: ( c = UAp c9 & c9 in Y ) by A14;

reconsider c = c as set by TARSKI:1;

A16: c c= the carrier of X by A15;

x in c by A14, A13;

hence x in the carrier of X by A16; :: thesis: verum

hence [(meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ),(meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } )] is RoughSet of X by Def13; :: thesis: verum

a9 in RoughSets X by Def20;

then reconsider a = a9 as Element of (RSLattice X) by Def23;

take a ; :: thesis: ( a is_less_than Y & ( for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a ) )

thus a is_less_than Y :: thesis: for b being Element of (RSLattice X) st b is_less_than Y holds

b [= a

proof

thus
for b being Element of (RSLattice X) st b is_less_than Y holds
let q be Element of (RSLattice X); :: according to LATTICE3:def 16 :: thesis: ( not q in Y or a [= q )

assume A17: q in Y ; :: thesis: a [= q

q in the carrier of (RSLattice X) ;

then q in RoughSets X by Def23;

then reconsider q9 = q as RoughSet of X by Def20;

consider q1, q2 being Subset of X such that

A18: q9 = [q1,q2] by Th55;

A19: q1 = LAp q9 by A18;

then A20: q1 in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by A17;

meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } c= LAp q9 by A19, A20, SETFAM_1:def 1;

then A21: LAp a9 c= LAp q9 ;

A22: UAp a9 = meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } ;

A23: q2 = UAp q9 by A18;

then A24: q2 in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by A17;

meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } c= UAp q9 by A23, A24, SETFAM_1:def 1;

hence a [= q by A21, Th71, A22; :: thesis: verum

end;assume A17: q in Y ; :: thesis: a [= q

q in the carrier of (RSLattice X) ;

then q in RoughSets X by Def23;

then reconsider q9 = q as RoughSet of X by Def20;

consider q1, q2 being Subset of X such that

A18: q9 = [q1,q2] by Th55;

A19: q1 = LAp q9 by A18;

then A20: q1 in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by A17;

meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } c= LAp q9 by A19, A20, SETFAM_1:def 1;

then A21: LAp a9 c= LAp q9 ;

A22: UAp a9 = meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } ;

A23: q2 = UAp q9 by A18;

then A24: q2 in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by A17;

meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } c= UAp q9 by A23, A24, SETFAM_1:def 1;

hence a [= q by A21, Th71, A22; :: thesis: verum

b [= a :: thesis: verum

proof

let b be Element of (RSLattice X); :: thesis: ( b is_less_than Y implies b [= a )

assume A25: b is_less_than Y ; :: thesis: b [= a

b is Element of RoughSets X by Def23;

then reconsider b9 = b as RoughSet of X by Def20;

reconsider a9 = a as RoughSet of X ;

A26: for q being Element of (RSLattice X) st q in Y holds

b [= q by A25;

for Z1 being set st Z1 in { (LAp a1) where a1 is RoughSet of X : a1 in Y } holds

LAp b9 c= Z1

A29: LAp b9 c= LAp a9 by A28;

for Z1 being set st Z1 in { (UAp a1) where a1 is RoughSet of X : a1 in Y } holds

UAp b9 c= Z1

UAp b9 c= UAp a9 by A31;

hence b [= a by A29, Th71; :: thesis: verum

end;assume A25: b is_less_than Y ; :: thesis: b [= a

b is Element of RoughSets X by Def23;

then reconsider b9 = b as RoughSet of X by Def20;

reconsider a9 = a as RoughSet of X ;

A26: for q being Element of (RSLattice X) st q in Y holds

b [= q by A25;

for Z1 being set st Z1 in { (LAp a1) where a1 is RoughSet of X : a1 in Y } holds

LAp b9 c= Z1

proof

then A28:
LAp b9 c= meet { (LAp a1) where a1 is RoughSet of X : a1 in Y }
by A5, SETFAM_1:5;
let Z1 be set ; :: thesis: ( Z1 in { (LAp a1) where a1 is RoughSet of X : a1 in Y } implies LAp b9 c= Z1 )

assume Z1 in { (LAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: LAp b9 c= Z1

then consider c1 being RoughSet of X such that

A27: ( Z1 = LAp c1 & c1 in Y ) ;

reconsider c19 = c1 as Element of (RSLattice X) by A27;

b [= c19 by A25, A27;

hence LAp b9 c= Z1 by A27, Th71; :: thesis: verum

end;assume Z1 in { (LAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: LAp b9 c= Z1

then consider c1 being RoughSet of X such that

A27: ( Z1 = LAp c1 & c1 in Y ) ;

reconsider c19 = c1 as Element of (RSLattice X) by A27;

b [= c19 by A25, A27;

hence LAp b9 c= Z1 by A27, Th71; :: thesis: verum

A29: LAp b9 c= LAp a9 by A28;

for Z1 being set st Z1 in { (UAp a1) where a1 is RoughSet of X : a1 in Y } holds

UAp b9 c= Z1

proof

then A31:
UAp b9 c= meet { (UAp a1) where a1 is RoughSet of X : a1 in Y }
by A7, SETFAM_1:5;
let Z1 be set ; :: thesis: ( Z1 in { (UAp a1) where a1 is RoughSet of X : a1 in Y } implies UAp b9 c= Z1 )

assume Z1 in { (UAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: UAp b9 c= Z1

then consider c2 being RoughSet of X such that

A30: ( Z1 = UAp c2 & c2 in Y ) ;

reconsider c29 = c2 as Element of (RSLattice X) by A30;

b [= c29 by A26, A30;

hence UAp b9 c= Z1 by A30, Th71; :: thesis: verum

end;assume Z1 in { (UAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: UAp b9 c= Z1

then consider c2 being RoughSet of X such that

A30: ( Z1 = UAp c2 & c2 in Y ) ;

reconsider c29 = c2 as Element of (RSLattice X) by A30;

b [= c29 by A26, A30;

hence UAp b9 c= Z1 by A30, Th71; :: thesis: verum

UAp b9 c= UAp a9 by A31;

hence b [= a by A29, Th71; :: thesis: verum

( b

( not b