for o being set st o in [:P,P:] holds
the L_join of L . o in P
proof
let o be set ; :: thesis: ( o in [:P,P:] implies the L_join of L . o in P )
assume o in [:P,P:] ; :: thesis: the L_join of L . o in P
then consider x, y being object such that
B1: ( x in P & y in P & o = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of L by B1;
the L_join of L . o = x "\/" y by B1;
hence the L_join of L . o in P by B1, LATTICES:def 25; :: thesis: verum
end;
then P is Preserv of the L_join of L by REALSET1:def 1;
then reconsider lj = the L_join of L || P as BinOp of P by REALSET1:2;
for o being set st o in [:P,P:] holds
the L_meet of L . o in P
proof
let o be set ; :: thesis: ( o in [:P,P:] implies the L_meet of L . o in P )
assume o in [:P,P:] ; :: thesis: the L_meet of L . o in P
then consider x, y being object such that
B1: ( x in P & y in P & o = [x,y] ) by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of L by B1;
the L_meet of L . o = x "/\" y by B1;
hence the L_meet of L . o in P by B1, LATTICES:def 24; :: thesis: verum
end;
then P is Preserv of the L_meet of L by REALSET1:def 1;
then reconsider lm = the L_meet of L || P as BinOp of P by REALSET1:2;
reconsider S = LattStr(# P,lj,lm #) as strict SubLattStr of L by Defx1;
take S ; :: thesis: the carrier of S = P
thus the carrier of S = P ; :: thesis: verum