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 ();
set A = the L_join of ();
set B = the L_meet of ();
A1: for x being Element of the carrier of () ex y being Element of the carrier of () st S1[x,y]
proof
let x be Element of the carrier of (); :: thesis: ex y being Element of the carrier of () st S1[x,y]
reconsider z = x as Subset of 3 by Th8;
A2: Segm 2 c= Segm 3 by NAT_1:39;
A3: Segm 1 c= Segm 3 by NAT_1:39;
now :: thesis: z ` in the carrier of ()
per cases ( z = 0 or z = 1 or z = 3 \ 1 or z = 3 \ 2 or z = 2 or z = 3 ) by ;
suppose z = 0 ; :: thesis: z ` in the carrier of ()
hence z ` in the carrier of () by ; :: thesis: verum
end;
suppose z = 1 ; :: thesis: z ` in the carrier of ()
hence z ` in the carrier of () by ; :: thesis: verum
end;
suppose z = 3 \ 1 ; :: thesis: z ` in the carrier of ()
then z ` = 3 /\ 1 by XBOOLE_1:48
.= 1 by ;
hence z ` in the carrier of () by ; :: thesis: verum
end;
suppose z = 3 \ 2 ; :: thesis: z ` in the carrier of ()
then z ` = 3 /\ 2 by XBOOLE_1:48
.= 2 by ;
hence z ` in the carrier of () by ; :: thesis: verum
end;
suppose z = 2 ; :: thesis: z ` in the carrier of ()
hence z ` in the carrier of () by ; :: thesis: verum
end;
suppose z = 3 ; :: thesis: z ` in the carrier of ()
then z ` = 0 by XBOOLE_1:37;
hence z ` in the carrier of () by ; :: thesis: verum
end;
end;
end;
then reconsider y = z ` as Element of the carrier of () ;
take y ; :: thesis: S1[x,y]
thus S1[x,y] ; :: thesis: verum
end;
ex f being Function of the carrier of (), the carrier of () st
for x being Element of the carrier of () holds S1[x,f . x] from then consider C being UnOp of the carrier of () such that
A4: for x being Element of the carrier of ()
for y being Subset of 3 st x = y holds
C . x = y ` ;
take OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #) ; :: thesis: ( LattStr(# the carrier of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #), the L_join of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #), the L_meet of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #) #) = latt B_6 & ( for x being Element of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #)
for y being Subset of 3 st x = y holds
the Compl of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #) . x = y ` ) )

thus ( LattStr(# the carrier of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #), the L_join of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #), the L_meet of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #) #) = latt B_6 & ( for x being Element of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #)
for y being Subset of 3 st x = y holds
the Compl of OrthoLattStr(# the carrier of (), the L_join of (), the L_meet of (),C #) . x = y ` ) ) by A4; :: thesis: verum