let X be Tolerance_Space; :: thesis:
let Y be Subset of (); :: according to VECTSP_8:def 6 :: thesis: ex b1 being Element of the carrier of () st
( b1 is_less_than Y & ( for b2 being Element of the carrier of () holds
( not b2 is_less_than Y or b2 [= b1 ) ) )

ex a being Element of () st
( a is_less_than Y & ( for b being Element of () 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 () st
( a is_less_than Y & ( for b being Element of () st b is_less_than Y holds
b [= a ) )

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

for q being Element of () st q in Y holds
a [= q by A1;
hence a is_less_than Y ; :: thesis: for b being Element of () st b is_less_than Y holds
b [= a

let b be Element of (); :: 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 () st
( a is_less_than Y & ( for b being Element of () 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 () by Def23;
then reconsider f = f as RoughSet of X by ;
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 () by Def23;
then reconsider g = g as RoughSet of X by ;
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 ;
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 ;
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 ;
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 ;
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 () by Def23;
take a ; :: thesis: ( a is_less_than Y & ( for b being Element of () st b is_less_than Y holds
b [= a ) )

thus a is_less_than Y :: thesis: for b being Element of () st b is_less_than Y holds
b [= a
proof
let q be Element of (); :: 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 () ;
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 ;
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 ;
hence a [= q by ; :: thesis: verum
end;
thus for b being Element of () st b is_less_than Y holds
b [= a :: thesis: verum
proof
let b be Element of (); :: 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 () 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 () by A27;
b [= c19 by ;
hence LAp b9 c= Z1 by ; :: thesis: verum
end;
then A28: LAp b9 c= meet { (LAp a1) where a1 is RoughSet of X : a1 in Y } by ;
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 () by A30;
b [= c29 by ;
hence UAp b9 c= Z1 by ; :: thesis: verum
end;
then A31: UAp b9 c= meet { (UAp a1) where a1 is RoughSet of X : a1 in Y } by ;
UAp b9 c= UAp a9 by A31;
hence b [= a by ; :: thesis: verum
end;
end;
end;
end;
hence ex b1 being Element of the carrier of () st
( b1 is_less_than Y & ( for b2 being Element of the carrier of () holds
( not b2 is_less_than Y or b2 [= b1 ) ) ) ; :: thesis: verum