defpred S1[ set , set ] means for y being Subset of 3 st $1 = y holds
$2 = y ` ;
set N = latt B_6;
set M = the carrier of (latt B_6);
set A = the L_join of (latt B_6);
set B = the L_meet of (latt B_6);
A1:
for x being Element of the carrier of (latt B_6) ex y being Element of the carrier of (latt B_6) st S1[x,y]
ex f being Function of the carrier of (latt B_6), the carrier of (latt B_6) st
for x being Element of the carrier of (latt B_6) holds S1[x,f . x]
from FUNCT_2:sch 3(A1);
then consider C being UnOp of the carrier of (latt B_6) such that
A4:
for x being Element of the carrier of (latt B_6)
for y being Subset of 3 st x = y holds
C . x = y `
;
take
OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #)
; ( LattStr(# the carrier of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #), the L_join of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #), the L_meet of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) #) = latt B_6 & ( for x being Element of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #)
for y being Subset of 3 st x = y holds
the Compl of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) . x = y ` ) )
thus
( LattStr(# the carrier of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #), the L_join of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #), the L_meet of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) #) = latt B_6 & ( for x being Element of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #)
for y being Subset of 3 st x = y holds
the Compl of OrthoLattStr(# the carrier of (latt B_6), the L_join of (latt B_6), the L_meet of (latt B_6),C #) . x = y ` ) )
by A4; verum