defpred S_{1}[ 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_{1}[x,y]

for x being Element of the carrier of (latt B_6) holds S_{1}[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

$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

proof

ex f being Function of the carrier of (latt B_6), the carrier of (latt B_6) st
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_{1}[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;

take y ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;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)end;

then reconsider y = z ` as Element of 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;

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;.= 1 by A3, XBOOLE_1:28 ;

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

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;.= 2 by A2, XBOOLE_1:28 ;

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

take y ; :: thesis: S

thus S

for x being Element of the carrier of (latt B_6) holds S

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