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 by LATTICE3:def 16; :: 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:45; :: 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 set such that
Z1: f in Y by A2, XBOOLE_0:def 1;
Y is Subset of (RoughSets X) by Def8;
then reconsider f = f as RoughSet of X by Z1, DefRSX;
b1: LAp f in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by Z1;
then B1: { (LAp a1) where a1 is RoughSet of X : a1 in Y } <> {} ;
consider g being set such that
Z2: g in Y by A2, XBOOLE_0:def 1;
Y is Subset of (RoughSets X) by Def8;
then reconsider g = g as RoughSet of X by Z2, DefRSX;
UAp g in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by Z2;
then B3: { (UAp a1) where a1 is RoughSet of X : a1 in Y } <> {} ;
X1: meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } c= the carrier of X

proof

let x be set ; :: 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 W1: 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
B2: c in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by b1;
consider c9 being RoughSet of X such that
B4: ( c = LAp c9 & c9 in Y ) by B2;
W2: c in bool the carrier of X by B4;
x in c by B2, W1;
hence x in the carrier of X by W2; :: 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 set ; :: 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 W1: 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 set such that
B2: c in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by B3, XBOOLE_0:def 1;
consider c9 being RoughSet of X such that
B4: ( c = UAp c9 & c9 in Y ) by B2;
W2: c c= the carrier of X by B4;
x in c by B2, W1;
hence x in the carrier of X by W2; :: 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 X1, ZFMISC_1:106;
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 Def19; :: 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 DefRSX;
then reconsider a = a9 as Element of (RSLattice X) by Def8;
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 AA: q in Y ; :: thesis: a [= q
q in the carrier of (RSLattice X) ;
then q in RoughSets X by Def8;
then reconsider q9 = q as RoughSet of X by DefRSX;
consider q1, q2 being Subset of X such that
A3: q9 = [q1,q2] by Def1;
A5: q1 = LAp q9 by A3, MCART_1:7;
then A4: q1 in { (LAp a1) where a1 is RoughSet of X : a1 in Y } by AA;
meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } c= LAp q9

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } or x in LAp q9 )
assume x in meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: x in LAp q9
hence x in LAp q9 by A5, A4, SETFAM_1:def 1; :: thesis: verum

end;

then A1: LAp a9 c= LAp q9 by MCART_1:7;
C2: UAp a9 = meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } by MCART_1:7;
C5: q2 = UAp q9 by A3, MCART_1:7;
then C4: q2 in { (UAp a1) where a1 is RoughSet of X : a1 in Y } by AA;
meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } c= UAp q9

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } or x in UAp q9 )
assume x in meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } ; :: thesis: x in UAp q9
hence x in UAp q9 by C5, C4, SETFAM_1:def 1; :: thesis: verum

end;

hence a [= q by A1, WazneX, C2; :: 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 K1: b is_less_than Y ; :: thesis: b [= a
b is Element of RoughSets X by Def8;
then reconsider b9 = b as RoughSet of X by DefRSX;
reconsider a9 = a as RoughSet of X ;
F0: for q being Element of (RSLattice X) st q in Y holds
b [= q by K1, LATTICE3:def 16;
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
F2: ( Z1 = LAp c1 & c1 in Y ) ;
reconsider c19 = c1 as Element of (RSLattice X) by F2;
b [= c19 by K1, LATTICE3:def 16, F2;
hence LAp b9 c= Z1 by F2, WazneX; :: thesis: verum

end;

then A2: LAp b9 c= meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } by B1, SETFAM_1:6;
meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } c= LAp a9 by MCART_1:7;
then B1: LAp b9 c= LAp a9 by A2, XBOOLE_1:1;
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
F3: ( Z1 = UAp c2 & c2 in Y ) ;
reconsider c29 = c2 as Element of (RSLattice X) by F3;
b [= c29 by F0, F3;
hence UAp b9 c= Z1 by F3, WazneX; :: thesis: verum

end;

then C2: UAp b9 c= meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } by B3, SETFAM_1:6;
meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } c= UAp a9 by MCART_1:7;
then UAp b9 c= UAp a9 by C2, XBOOLE_1:1;
hence b [= a by B1, WazneX; :: 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