defpred S₁[ 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 S₁[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 S₁[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 = 0 ; :: thesis: z ` in the carrier of (latt B_6)

hence z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def 4; :: thesis: verum

end;

suppose z = 1 ; :: thesis: z ` in the carrier of (latt B_6)

hence z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def 4; :: thesis: verum

end;

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;

suppose z = 2 ; :: thesis: z ` in the carrier of (latt B_6)

hence z ` in the carrier of (latt B_6) by Th7, ENUMSET1:def 4; :: thesis: verum

end;

suppose z = 3 ; :: thesis: z ` in the carrier of (latt B_6)

then z ` = 0 by XBOOLE_1:37;
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: S₁[x,y]
thus S₁[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 S₁[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