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]
proof
let x be Element of the carrier of (latt B_6); :: thesis: ex y being Element of the carrier of (latt B_6) 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 (latt B_6)
per cases ( z = 0 or z = 1 or z = 3 \ 1 or z = 3 \ 2 or z = 2 or z = 3 ) by Th7, ENUMSET1:def 4;
suppose z = 3 \ 1 ; :: thesis: z ` in the carrier of (latt B_6)
then z ` = 3 /\ 1 by XBOOLE_1:48
.= 1 by A3, XBOOLE_1:28 ;
hence z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def 4; :: thesis: verum
end;
suppose z = 3 \ 2 ; :: thesis: z ` in the carrier of (latt B_6)
then z ` = 3 /\ 2 by XBOOLE_1:48
.= 2 by A2, XBOOLE_1:28 ;
hence z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def 4; :: thesis: verum
end;
end;
end;
then reconsider y = z ` as Element of the carrier of (latt B_6) ;
take y ; :: thesis: S1[x,y]
thus S1[x,y] ; :: thesis: verum
end;
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 #) ; :: thesis: ( 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; :: thesis: verum