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₁ being Element of the carrier of (RSLattice X) st
( b₁ is_less_than Y & ( for b₂ being Element of the carrier of (RSLattice X) holds
( not b₂ is_less_than Y or b₂ [= 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

per cases ( Y is empty or not Y is empty ) ;

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 ) )

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;

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 ) )

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

proof

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;

[(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

proof

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

proof

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;

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;
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;

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 ;
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

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;

thus for b being Element of (RSLattice X) st b is_less_than Y holds
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

proof

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;

then A28: LAp b9 c= meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } by A5, SETFAM_1:5;
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

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;

then A31: UAp b9 c= meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } by A7, SETFAM_1:5;
UAp b9 c= UAp a9 by A31;
hence b [= a by A29, Th71; :: thesis: verum

end;

end;

end;

end;

hence ex b₁ being Element of the carrier of (RSLattice X) st
( b₁ is_less_than Y & ( for b₂ being Element of the carrier of (RSLattice X) holds
( not b₂ is_less_than Y or b₂ [= b₁ ) ) ) ; :: thesis: verum