set L = LattStr(# {1,2,3},example32\/,example32/\ #);
take LattStr(# {1,2,3},example32\/,example32/\ #) ; :: thesis: ( ( for x being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( x = 1 or x = 2 or x = 3 ) ) & ( for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( ( not x "/\" y = 1 or y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies x "/\" y = 1 ) & ( x "/\" y = 2 implies ( x = 2 & y = 2 ) ) & ( x = 2 & y = 2 implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) ) ) & ( for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( ( x "\/" y = 1 implies ( x = 1 & ( y = 1 or y = 3 ) ) ) & ( x = 1 & ( y = 1 or y = 3 ) implies x "\/" y = 1 ) & ( not x "\/" y = 2 or x = 2 or ( x = 1 & y = 2 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) ) ) & LattStr(# {1,2,3},example32\/,example32/\ #) is GAD_Lattice & LattStr(# {1,2,3},example32\/,example32/\ #) is not AD_Lattice )
thus for x being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1; :: thesis: ( ( for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( ( not x "/\" y = 1 or y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies x "/\" y = 1 ) & ( x "/\" y = 2 implies ( x = 2 & y = 2 ) ) & ( x = 2 & y = 2 implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) ) ) & ( for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( ( x "\/" y = 1 implies ( x = 1 & ( y = 1 or y = 3 ) ) ) & ( x = 1 & ( y = 1 or y = 3 ) implies x "\/" y = 1 ) & ( not x "\/" y = 2 or x = 2 or ( x = 1 & y = 2 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) ) ) & LattStr(# {1,2,3},example32\/,example32/\ #) is GAD_Lattice & LattStr(# {1,2,3},example32\/,example32/\ #) is not AD_Lattice )
thus Z7: for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( ( not x "/\" y = 1 or y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies x "/\" y = 1 ) & ( x "/\" y = 2 implies ( x = 2 & y = 2 ) ) & ( x = 2 & y = 2 implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) ) :: thesis: ( ( for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( ( x "\/" y = 1 implies ( x = 1 & ( y = 1 or y = 3 ) ) ) & ( x = 1 & ( y = 1 or y = 3 ) implies x "\/" y = 1 ) & ( not x "\/" y = 2 or x = 2 or ( x = 1 & y = 2 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) ) ) & LattStr(# {1,2,3},example32\/,example32/\ #) is GAD_Lattice & LattStr(# {1,2,3},example32\/,example32/\ #) is not AD_Lattice )

proof

let x, y be Element of LattStr(# {1,2,3},example32\/,example32/\ #); :: thesis: ( ( not x "/\" y = 1 or y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies x "/\" y = 1 ) & ( x "/\" y = 2 implies ( x = 2 & y = 2 ) ) & ( x = 2 & y = 2 implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) )
reconsider x1 = x, y1 = y as Element of {1,2,3} ;
B1: x "/\" y = x1 example32"/\" y1 by Defx8;
thus ( x "/\" y = 1 iff ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) ) :: thesis: ( ( x "/\" y = 2 implies ( x = 2 & y = 2 ) ) & ( x = 2 & y = 2 implies x "/\" y = 2 ) & ( x "/\" y = 3 implies y = 3 ) & ( y = 3 implies x "/\" y = 3 ) )

proof

hereby :: thesis: ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) implies x "/\" y = 1 )

assume B3: x "/\" y = 1 ; :: thesis: ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) )
assume ( not y = 1 & not ( y = 2 & ( x = 1 or x = 3 ) ) ) ; :: thesis: contradiction
then ( ( x = 2 & y = 2 ) or y = 3 ) by ENUMSET1:def 1;
hence contradiction by B3, B1, Defx5; :: thesis: verum

end;

assume ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) ; :: thesis: x "/\" y = 1
hence x "/\" y = 1 by B1, Defx5; :: thesis: verum

end;

thus ( x "/\" y = 2 iff ( x = 2 & y = 2 ) ) :: thesis: ( x "/\" y = 3 iff y = 3 )

proof

hereby :: thesis: ( x = 2 & y = 2 implies x "/\" y = 2 )

assume B3: x "/\" y = 2 ; :: thesis: ( x = 2 & y = 2 )
assume ( not x = 2 or not y = 2 ) ; :: thesis: contradiction
then ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) or y = 3 ) by ENUMSET1:def 1;
hence contradiction by B3, B1, Defx5; :: thesis: verum

end;

assume ( x = 2 & y = 2 ) ; :: thesis: x "/\" y = 2
hence x "/\" y = 2 by B1, Defx5; :: thesis: verum

end;

thus ( x "/\" y = 3 iff y = 3 ) :: thesis: verum

proof

hereby :: thesis: ( y = 3 implies x "/\" y = 3 )

assume B3: x "/\" y = 3 ; :: thesis: y = 3
assume not y = 3 ; :: thesis: contradiction
then ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) or ( x = 2 & y = 2 ) ) by ENUMSET1:def 1;
hence contradiction by B3, B1, Defx5; :: thesis: verum

end;

assume y = 3 ; :: thesis: x "/\" y = 3
hence x "/\" y = 3 by B1, Defx5; :: thesis: verum

end;

end;

thus Z8: for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds
( ( x "\/" y = 1 implies ( x = 1 & ( y = 1 or y = 3 ) ) ) & ( x = 1 & ( y = 1 or y = 3 ) implies x "\/" y = 1 ) & ( not x "\/" y = 2 or x = 2 or ( x = 1 & y = 2 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) ) :: thesis: ( LattStr(# {1,2,3},example32\/,example32/\ #) is GAD_Lattice & LattStr(# {1,2,3},example32\/,example32/\ #) is not AD_Lattice )

proof

let x, y be Element of LattStr(# {1,2,3},example32\/,example32/\ #); :: thesis: ( ( x "\/" y = 1 implies ( x = 1 & ( y = 1 or y = 3 ) ) ) & ( x = 1 & ( y = 1 or y = 3 ) implies x "\/" y = 1 ) & ( not x "\/" y = 2 or x = 2 or ( x = 1 & y = 2 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) )
reconsider x1 = x, y1 = y as Element of {1,2,3} ;
B1: x "\/" y = x1 example32"\/" y1 by Defx7;
thus ( x "\/" y = 1 iff ( x = 1 & ( y = 1 or y = 3 ) ) ) :: thesis: ( ( not x "\/" y = 2 or x = 2 or ( x = 1 & y = 2 ) ) & ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 ) & ( x "\/" y = 3 implies x = 3 ) & ( x = 3 implies x "\/" y = 3 ) )

proof

hereby :: thesis: ( x = 1 & ( y = 1 or y = 3 ) implies x "\/" y = 1 )

assume B3: x "\/" y = 1 ; :: thesis: ( x = 1 & ( y = 1 or y = 3 ) )
assume ( not x = 1 or ( not y = 1 & not y = 3 ) ) ; :: thesis: contradiction
then ( x = 2 or ( x = 1 & y = 2 ) or x = 3 ) by ENUMSET1:def 1;
hence contradiction by B3, B1, Defx6; :: thesis: verum

end;

assume ( x = 1 & ( y = 1 or y = 3 ) ) ; :: thesis: x "\/" y = 1
hence x "\/" y = 1 by B1, Defx6; :: thesis: verum

end;

thus ( x "\/" y = 2 iff ( x = 2 or ( x = 1 & y = 2 ) ) ) :: thesis: ( x "\/" y = 3 iff x = 3 )

proof

hereby :: thesis: ( ( x = 2 or ( x = 1 & y = 2 ) ) implies x "\/" y = 2 )

assume B3: x "\/" y = 2 ; :: thesis: ( x = 2 or ( x = 1 & y = 2 ) )
assume ( not x = 2 & not ( x = 1 & y = 2 ) ) ; :: thesis: contradiction
then ( ( x = 1 & ( y = 1 or y = 3 ) ) or x = 3 ) by ENUMSET1:def 1;
hence contradiction by B3, B1, Defx6; :: thesis: verum

end;

assume ( x = 2 or ( x = 1 & y = 2 ) ) ; :: thesis: x "\/" y = 2
hence x "\/" y = 2 by B1, Defx6; :: thesis: verum

end;

thus ( x "\/" y = 3 iff x = 3 ) :: thesis: verum

proof

hereby :: thesis: ( x = 3 implies x "\/" y = 3 )

assume B3: x "\/" y = 3 ; :: thesis: x = 3
assume not x = 3 ; :: thesis: contradiction
then ( ( x = 1 & ( y = 1 or y = 3 ) ) or x = 2 or ( x = 1 & y = 2 ) ) by ENUMSET1:def 1;
hence contradiction by B3, B1, Defx6; :: thesis: verum

end;

assume x = 3 ; :: thesis: x "\/" y = 3
hence x "\/" y = 3 by B1, Defx6; :: thesis: verum

end;

end;

for x, y, z being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds x "/\" (y "/\" z) = (x "/\" y) "/\" z

proof

let x, y, z be Element of LattStr(# {1,2,3},example32\/,example32/\ #); :: thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z

per cases ( x "/\" (y "/\" z) = 1 or x "/\" (y "/\" z) = 2 or x "/\" (y "/\" z) = 3 ) by ENUMSET1:def 1;

suppose B1: x "/\" (y "/\" z) = 1 ; :: thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z

then ( y "/\" z = 1 or ( y "/\" z = 2 & ( x = 1 or x = 3 ) ) ) by Z7;
then ( z = 1 or ( z = 2 & ( y = 1 or y = 3 ) ) or ( y = 2 & z = 2 & ( x = 1 or x = 3 ) ) ) by Z7;
then ( z = 1 or ( z = 2 & ( x "/\" y = 1 or x "/\" y = 3 ) ) ) by Z7;
hence x "/\" (y "/\" z) = (x "/\" y) "/\" z by B1, Z7; :: thesis: verum

end;

suppose B1: x "/\" (y "/\" z) = 2 ; :: thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z

then ( x = 2 & y "/\" z = 2 ) by Z7;
then ( x = 2 & y = 2 & z = 2 ) by Z7;
then ( x "/\" y = 2 & z = 2 ) by Z7;
hence x "/\" (y "/\" z) = (x "/\" y) "/\" z by B1, Z7; :: thesis: verum

end;

suppose B1: x "/\" (y "/\" z) = 3 ; :: thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z

then y "/\" z = 3 by Z7;
then z = 3 by Z7;
hence x "/\" (y "/\" z) = (x "/\" y) "/\" z by B1, Z7; :: thesis: verum

end;

end;

end;

then C1: LattStr(# {1,2,3},example32\/,example32/\ #) is meet-associative ;
for x, y, z being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

proof

let x, y, z be Element of LattStr(# {1,2,3},example32\/,example32/\ #); :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

per cases ( x "/\" (y "\/" z) = 1 or x "/\" (y "\/" z) = 2 or x "/\" (y "\/" z) = 3 ) by ENUMSET1:def 1;

suppose B1: x "/\" (y "\/" z) = 1 ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

( y "\/" z = 1 or ( y "\/" z = 2 & ( x = 1 or x = 3 ) ) ) by B1, Z7;
then ( ( y = 1 or ( y = 2 & ( x = 1 or x = 3 ) ) ) & ( z = 1 or ( z = 2 & ( x = 1 or x = 3 ) ) or z = 3 ) ) by Z8, ENUMSET1:def 1;
then ( x "/\" y = 1 & ( x "/\" z = 1 or z = 3 ) ) by Z7;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by B1, Z7, Z8; :: thesis: verum

end;

suppose B1: x "/\" (y "\/" z) = 2 ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then ( x = 2 & y "\/" z = 2 ) by Z7;
then ( x = 2 & ( y = 2 or ( y = 1 & z = 2 ) ) ) by Z8;
then ( x "/\" y = 2 or ( x "/\" y = 1 & x "/\" z = 2 ) ) by Z7;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by B1, Z8; :: thesis: verum

end;

suppose B1: x "/\" (y "\/" z) = 3 ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then y "\/" z = 3 by Z7;
then x "/\" y = 3 by Z7, Z8;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by B1, Z8; :: thesis: verum

end;

end;

end;

then C2: LattStr(# {1,2,3},example32\/,example32/\ #) is distributive ;
for x, y, z being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)

proof

let x, y, z be Element of LattStr(# {1,2,3},example32\/,example32/\ #); :: thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)

per cases ( x "\/" (y "/\" z) = 1 or x "\/" (y "/\" z) = 2 or x "\/" (y "/\" z) = 3 ) by ENUMSET1:def 1;

suppose B1: x "\/" (y "/\" z) = 1 ; :: thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)

then ( x = 1 & ( y "/\" z = 1 or y "/\" z = 3 ) ) by Z8;
then ( x = 1 & ( z = 1 or ( z = 2 & ( y = 1 or y = 3 ) ) or z = 3 ) ) by Z7;
then ( x "\/" z = 1 or ( x "\/" z = 2 & ( x "\/" y = 1 or x "\/" y = 3 ) ) ) by Z8;
hence x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) by B1, Z7; :: thesis: verum

end;

suppose B1: x "\/" (y "/\" z) = 2 ; :: thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)

then ( x = 2 or ( x = 1 & y "/\" z = 2 ) ) by Z8;
then ( x = 2 or ( x = 1 & y = 2 & z = 2 ) ) by Z7;
then ( x "\/" y = 2 & x "\/" z = 2 ) by Z8;
hence x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) by B1, Z7; :: thesis: verum

end;

suppose B1: x "\/" (y "/\" z) = 3 ; :: thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)

then x = 3 by Z8;
then x "\/" z = 3 by Z8;
hence x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) by B1, Z7; :: thesis: verum

end;

end;

end;

then C3: LattStr(# {1,2,3},example32\/,example32/\ #) is left-Distributive ;
for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds x "/\" (x "\/" y) = x

proof

let x, y be Element of LattStr(# {1,2,3},example32\/,example32/\ #); :: thesis: x "/\" (x "\/" y) = x

per cases ( x "/\" (x "\/" y) = 1 or x "/\" (x "\/" y) = 2 or x "/\" (x "\/" y) = 3 ) by ENUMSET1:def 1;

suppose B1: x "/\" (x "\/" y) = 1 ; :: thesis: x "/\" (x "\/" y) = x

then ( x "\/" y = 1 or ( x "\/" y = 2 & ( x = 1 or x = 3 ) ) ) by Z7;
hence x "/\" (x "\/" y) = x by B1, Z8; :: thesis: verum

end;

suppose x "/\" (x "\/" y) = 2 ; :: thesis: x "/\" (x "\/" y) = x

hence x "/\" (x "\/" y) = x by Z7; :: thesis: verum

end;

suppose B1: x "/\" (x "\/" y) = 3 ; :: thesis: x "/\" (x "\/" y) = x

then x "\/" y = 3 by Z7;
hence x "/\" (x "\/" y) = x by B1, Z8; :: thesis: verum

end;

end;

end;

then C4: LattStr(# {1,2,3},example32\/,example32/\ #) is join-absorbing ;
for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds (x "\/" y) "/\" x = x

proof

let x, y be Element of LattStr(# {1,2,3},example32\/,example32/\ #); :: thesis: (x "\/" y) "/\" x = x

per cases ( (x "\/" y) "/\" x = 1 or (x "\/" y) "/\" x = 2 or (x "\/" y) "/\" x = 3 ) by ENUMSET1:def 1;

suppose B1: (x "\/" y) "/\" x = 1 ; :: thesis: (x "\/" y) "/\" x = x

then ( x = 1 or ( x = 2 & ( x "\/" y = 1 or x "\/" y = 3 ) ) ) by Z7;
hence (x "\/" y) "/\" x = x by B1, Z8; :: thesis: verum

end;

suppose (x "\/" y) "/\" x = 2 ; :: thesis: (x "\/" y) "/\" x = x

hence (x "\/" y) "/\" x = x by Z7; :: thesis: verum

end;

suppose (x "\/" y) "/\" x = 3 ; :: thesis: (x "\/" y) "/\" x = x

hence (x "\/" y) "/\" x = x by Z7; :: thesis: verum

end;

end;

end;

then C5: LattStr(# {1,2,3},example32\/,example32/\ #) is Meet-Absorbing ;
for x, y being Element of LattStr(# {1,2,3},example32\/,example32/\ #) holds (x "/\" y) "\/" y = y

proof

let x, y be Element of LattStr(# {1,2,3},example32\/,example32/\ #); :: thesis: (x "/\" y) "\/" y = y

per cases ( (x "/\" y) "\/" y = 1 or (x "/\" y) "\/" y = 2 or (x "/\" y) "\/" y = 3 ) by ENUMSET1:def 1;

suppose B1: (x "/\" y) "\/" y = 1 ; :: thesis: (x "/\" y) "\/" y = y

then ( x "/\" y = 1 & ( y = 1 or y = 3 ) ) by Z8;
hence (x "/\" y) "\/" y = y by B1, Z7; :: thesis: verum

end;

suppose B1: (x "/\" y) "\/" y = 2 ; :: thesis: (x "/\" y) "\/" y = y

then ( x "/\" y = 2 or ( x "/\" y = 1 & y = 2 ) ) by Z8;
hence (x "/\" y) "\/" y = y by Z7, B1; :: thesis: verum

end;

suppose B1: (x "/\" y) "\/" y = 3 ; :: thesis: (x "/\" y) "\/" y = y

then x "/\" y = 3 by Z8;
hence (x "/\" y) "\/" y = y by B1, Z7; :: thesis: verum

end;

end;

end;

then C6: LattStr(# {1,2,3},example32\/,example32/\ #) is meet-absorbing ;
not LattStr(# {1,2,3},example32\/,example32/\ #) is Meet-absorbing

proof

assume B1: LattStr(# {1,2,3},example32\/,example32/\ #) is Meet-absorbing ; :: thesis: contradiction
set x = 3;
set y = 2;
reconsider x = 3, y = 2 as Element of LattStr(# {1,2,3},example32\/,example32/\ #) by ENUMSET1:def 1;
(x "\/" y) "/\" y = 1 by Z7, Z8;
hence contradiction by B1; :: thesis: verum

end;

hence ( LattStr(# {1,2,3},example32\/,example32/\ #) is GAD_Lattice & LattStr(# {1,2,3},example32\/,example32/\ #) is not AD_Lattice ) by C1, C2, C3, C4, C5, C6; :: thesis: verum