set S = B squared ;
AA: for p, q being Element of [:B,B:] st p in B squared & q in B squared holds
p "\/" q in B squared

proof

let p, q be Element of [:B,B:]; :: thesis: ( p in B squared & q in B squared implies p "\/" q in B squared )
assume A0: ( p in B squared & q in B squared ) ; :: thesis: p "\/" q in B squared
then consider a1, b1 being Element of B such that
A1: ( p = [a1,b1] & a1 [= b1 ) ;
consider a2, b2 being Element of B such that
A2: ( q = [a2,b2] & a2 [= b2 ) by A0;
A3: p "\/" q = [(a1 "\/" a2),(b1 "\/" b2)] by FILTER_1:35, A1, A2;
a1 "\/" a2 [= b1 "\/" b2 by A1, A2, FILTER_0:4;
hence p "\/" q in B squared by A3; :: thesis: verum

end;

for p, q being Element of [:B,B:] st p in B squared & q in B squared holds
p "/\" q in B squared

proof

let p, q be Element of [:B,B:]; :: thesis: ( p in B squared & q in B squared implies p "/\" q in B squared )
assume A0: ( p in B squared & q in B squared ) ; :: thesis: p "/\" q in B squared
then consider a1, b1 being Element of B such that
A1: ( p = [a1,b1] & a1 [= b1 ) ;
consider a2, b2 being Element of B such that
A2: ( q = [a2,b2] & a2 [= b2 ) by A0;
A3: p "/\" q = [(a1 "/\" a2),(b1 "/\" b2)] by FILTER_1:35, A1, A2;
a1 "/\" a2 [= b1 "/\" b2 by A1, A2, FILTER_0:5;
hence p "/\" q in B squared by A3; :: thesis: verum

end;

hence ( B squared is join-closed & B squared is meet-closed ) by LATTICES:def 24, LATTICES:def 25, AA; :: thesis: verum