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

let b be Element of (BoolePoset X); :: thesis: ( b is_<=_than Y implies Me >= b )
assume A3: b is_<=_than Y ; :: thesis: Me >= b

now

let Z be set ; :: thesis: ( Z in Y implies b c= Z )
assume A4: Z in Y ; :: thesis: b c= Z
then reconsider Z9 = Z as Element of (BoolePoset X) ;
b <= Z9 by A3, A4, LATTICE3:def 8;
hence b c= Z by Th2; :: thesis: verum

end;

then b c= Me by SETFAM_1:5;
hence Me >= b by Th2; :: thesis: verum

end;

now

let b be Element of (BoolePoset X); :: thesis: ( b in Y implies Me <= b )
assume b in Y ; :: thesis: Me <= b
then Me c= b by SETFAM_1:3;
hence Me <= b by Th2; :: thesis: verum

end;

then Me is_<=_than Y by LATTICE3:def 8;
hence inf Y = meet Y by A2, YELLOW_0:33; :: thesis: verum