reconsider W = [#] REAL as Subset of REAL ;
let IT be Subset of REAL; :: thesis: for b₁ being real-membered set st IT = meet { A where A is Subset of REAL : ( b₁ c= A & A is closed ) } holds
IT = meet { A where A is Subset of REAL : ( IT c= A & A is closed ) }
let X be real-membered set ; :: thesis: ( IT = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } implies IT = meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } )
set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
set ClIT = { A where A is Subset of REAL : ( IT c= A & A is closed ) } ;
assume A1: IT = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ; :: thesis: IT = meet { A where A is Subset of REAL : ( IT c= A & A is closed ) }
X c= W by MEMBERED:3;
then A2: W in { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
A3: W in { A where A is Subset of REAL : ( IT c= A & A is closed ) } ;
thus IT c= meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } :: according to XBOOLE_0:def 10 :: thesis: meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } c= IT

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in IT or e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } )
assume A4: e in IT ; :: thesis: e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) }
for Y being set st Y in { A where A is Subset of REAL : ( IT c= A & A is closed ) } holds
e in Y

proof

let Y be set ; :: thesis: ( Y in { A where A is Subset of REAL : ( IT c= A & A is closed ) } implies e in Y )
assume Y in { A where A is Subset of REAL : ( IT c= A & A is closed ) } ; :: thesis: e in Y
then consider A being Subset of REAL such that
A5: A = Y and
A6: IT c= A and
A7: A is closed ;
for Z being set st Z in { A where A is Subset of REAL : ( X c= A & A is closed ) } holds
X c= Z

proof

let Z be set ; :: thesis: ( Z in { A where A is Subset of REAL : ( X c= A & A is closed ) } implies X c= Z )
assume Z in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; :: thesis: X c= Z
then ex B being Subset of REAL st
( Z = B & X c= B & B is closed ) ;
hence X c= Z ; :: thesis: verum

end;

then X c= IT by A1, A2, SETFAM_1:5;
then X c= A by A6;
then A in { A where A is Subset of REAL : ( X c= A & A is closed ) } by A7;
hence e in Y by A1, A4, A5, SETFAM_1:def 1; :: thesis: verum

end;

hence e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } by A3, SETFAM_1:def 1; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } or e in IT )
assume A8: e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } ; :: thesis: e in IT
for Y being set st Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } holds
e in Y

proof

let Y be set ; :: thesis: ( Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } implies e in Y )
assume A9: Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; :: thesis: e in Y
then consider A being Subset of REAL such that
A10: A = Y and
X c= A and
A11: A is closed ;
IT c= A by A1, A9, A10, SETFAM_1:3;
then A in { A where A is Subset of REAL : ( IT c= A & A is closed ) } by A11;
hence e in Y by A8, A10, SETFAM_1:def 1; :: thesis: verum

end;

hence e in IT by A1, A2, SETFAM_1:def 1; :: thesis: verum