let X be set ; :: thesis: for Y being non empty Subset of (BoolePoset X) holds inf Y = meet Y
set L = BoolePoset X;
let Y be non empty Subset of (BoolePoset X); :: thesis: inf Y = meet Y
set y = the Element of Y;
A1: the carrier of (BoolePoset X) = bool X by LATTICE3:def 1;
then the Element of Y c= X ;
then reconsider Me = meet Y as Element of (BoolePoset X) by A1, SETFAM_1:7;

A2: now :: thesis: for b being Element of (BoolePoset X) st b is_<=_than Y holds
Me >= b

let b be Element of (BoolePoset X); :: thesis: ( b is_<=_than Y implies Me >= b )
assume A3: b is_<=_than Y ; :: thesis: Me >= b
for Z being set st Z in Y holds
b c= Z by Th2, A3;
then b c= Me by SETFAM_1:5;
hence Me >= b by Th2; :: thesis: verum

end;

for b being Element of (BoolePoset X) st b in Y holds
Me <= b by Th2, SETFAM_1:3;
then Me is_<=_than Y ;
hence inf Y = meet Y by A2, YELLOW_0:33; :: thesis: verum