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: 2 c= 3 by NAT_1:40;
A3: 1 c= 3 by NAT_1:40;

now

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 IT = 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 IT,the L_join of IT,the L_meet of IT #) = latt B_6 & ( for x being Element of IT
for y being Subset of 3 st x = y holds
the Compl of IT . x = y ` ) )
thus ( LattStr(# the carrier of IT,the L_join of IT,the L_meet of IT #) = latt B_6 & ( for x being Element of IT
for y being Subset of 3 st x = y holds
the Compl of IT . x = y ` ) ) by A4; :: thesis: verum