let L be non empty LattStr ; :: thesis: for S being non empty ClosedSubset of L holds
( ( L is meet-associative implies latt (L,S) is meet-associative ) & ( L is meet-absorbing implies latt (L,S) is meet-absorbing ) & ( L is meet-commutative implies latt (L,S) is meet-commutative ) & ( L is join-associative implies latt (L,S) is join-associative ) & ( L is join-absorbing implies latt (L,S) is join-absorbing ) & ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
let S be non empty ClosedSubset of L; :: thesis: ( ( L is meet-associative implies latt (L,S) is meet-associative ) & ( L is meet-absorbing implies latt (L,S) is meet-absorbing ) & ( L is meet-commutative implies latt (L,S) is meet-commutative ) & ( L is join-associative implies latt (L,S) is join-associative ) & ( L is join-absorbing implies latt (L,S) is join-absorbing ) & ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
thus ( L is meet-associative implies latt (L,S) is meet-associative ) :: thesis: ( ( L is meet-absorbing implies latt (L,S) is meet-absorbing ) & ( L is meet-commutative implies latt (L,S) is meet-commutative ) & ( L is join-associative implies latt (L,S) is join-associative ) & ( L is join-absorbing implies latt (L,S) is join-absorbing ) & ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
proof
assume Z2: L is meet-associative ; :: thesis: latt (L,S) is meet-associative
let a, b, c be Element of (latt (L,S)); :: according to LATTICES:def 7 :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider x = a, y = b, z = c as Element of L by Defx1, TARSKI:def 3;
( b "/\" c = y "/\" z & a "/\" b = x "/\" y ) by Thx4;
then ( a "/\" (b "/\" c) = x "/\" (y "/\" z) & (a "/\" b) "/\" c = (x "/\" y) "/\" z ) by Thx4;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c by Z2; :: thesis: verum
end;
thus ( L is meet-absorbing implies latt (L,S) is meet-absorbing ) :: thesis: ( ( L is meet-commutative implies latt (L,S) is meet-commutative ) & ( L is join-associative implies latt (L,S) is join-associative ) & ( L is join-absorbing implies latt (L,S) is join-absorbing ) & ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
proof
assume Z3: L is meet-absorbing ; :: thesis: latt (L,S) is meet-absorbing
let a, b be Element of (latt (L,S)); :: according to LATTICES:def 8 :: thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of L by Defx1, TARSKI:def 3;
a "/\" b = x "/\" y by Thx4;
then (a "/\" b) "\/" b = (x "/\" y) "\/" y by Thx3;
hence (a "/\" b) "\/" b = b by Z3; :: thesis: verum
end;
thus ( L is meet-commutative implies latt (L,S) is meet-commutative ) :: thesis: ( ( L is join-associative implies latt (L,S) is join-associative ) & ( L is join-absorbing implies latt (L,S) is join-absorbing ) & ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
proof
assume Z3: L is meet-commutative ; :: thesis: latt (L,S) is meet-commutative
let a, b be Element of (latt (L,S)); :: according to LATTICES:def 6 :: thesis: a "/\" b = b "/\" a
reconsider x = a, y = b as Element of L by Defx1, TARSKI:def 3;
( a "/\" b = x "/\" y & b "/\" a = y "/\" x ) by Thx4;
hence a "/\" b = b "/\" a by Z3; :: thesis: verum
end;
thus ( L is join-associative implies latt (L,S) is join-associative ) :: thesis: ( ( L is join-absorbing implies latt (L,S) is join-absorbing ) & ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
proof
assume Z3: L is join-associative ; :: thesis: latt (L,S) is join-associative
let a, b, c be Element of (latt (L,S)); :: according to LATTICES:def 5 :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider x = a, y = b, z = c as Element of L by Defx1, TARSKI:def 3;
( b "\/" c = y "\/" z & a "\/" b = x "\/" y ) by Thx3;
then ( a "\/" (b "\/" c) = x "\/" (y "\/" z) & (a "\/" b) "\/" c = (x "\/" y) "\/" z ) by Thx3;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c by Z3; :: thesis: verum
end;
thus ( L is join-absorbing implies latt (L,S) is join-absorbing ) :: thesis: ( ( L is join-commutative implies latt (L,S) is join-commutative ) & ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
proof
assume Z3: L is join-absorbing ; :: thesis: latt (L,S) is join-absorbing
let a, b be Element of (latt (L,S)); :: according to LATTICES:def 9 :: thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of L by Defx1, TARSKI:def 3;
a "\/" b = x "\/" y by Thx3;
then a "/\" (a "\/" b) = x "/\" (x "\/" y) by Thx4;
hence a "/\" (a "\/" b) = a by Z3; :: thesis: verum
end;
thus ( L is join-commutative implies latt (L,S) is join-commutative ) :: thesis: ( ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) & ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
proof
assume Z3: L is join-commutative ; :: thesis: latt (L,S) is join-commutative
let a, b be Element of (latt (L,S)); :: according to LATTICES:def 4 :: thesis: a "\/" b = b "\/" a
reconsider x = a, y = b as Element of L by Defx1, TARSKI:def 3;
( a "\/" b = x "\/" y & b "\/" a = y "\/" x ) by Thx3;
hence a "\/" b = b "\/" a by Z3; :: thesis: verum
end;
thus ( L is Meet-Absorbing implies latt (L,S) is Meet-Absorbing ) :: thesis: ( ( L is distributive implies latt (L,S) is distributive ) & ( L is left-Distributive implies latt (L,S) is left-Distributive ) )
proof
assume Z3: L is Meet-Absorbing ; :: thesis: latt (L,S) is Meet-Absorbing
let a, b be Element of (latt (L,S)); :: according to LATTAD_1:def 3 :: thesis: (a "\/" b) "/\" a = a
reconsider x = a, y = b as Element of L by Defx1, TARSKI:def 3;
a "\/" b = x "\/" y by Thx3;
then (a "\/" b) "/\" a = (x "\/" y) "/\" x by Thx4;
hence (a "\/" b) "/\" a = a by Z3; :: thesis: verum
end;
thus ( L is distributive implies latt (L,S) is distributive ) :: thesis: ( L is left-Distributive implies latt (L,S) is left-Distributive )
proof
assume Z3: L is distributive ; :: thesis: latt (L,S) is distributive
let a, b, c be Element of (latt (L,S)); :: according to LATTICES:def 11 :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
reconsider x = a, y = b, z = c as Element of L by Defx1, TARSKI:def 3;
( b "\/" c = y "\/" z & a "/\" b = x "/\" y & a "/\" c = x "/\" z ) by Thx3, Thx4;
then ( a "/\" (b "\/" c) = x "/\" (y "\/" z) & (a "/\" b) "\/" (a "/\" c) = (x "/\" y) "\/" (x "/\" z) ) by Thx3, Thx4;
hence a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by Z3; :: thesis: verum
end;
thus ( L is left-Distributive implies latt (L,S) is left-Distributive ) :: thesis: verum
proof
assume Z3: L is left-Distributive ; :: thesis: latt (L,S) is left-Distributive
let a, b, c be Element of (latt (L,S)); :: according to LATTAD_1:def 4 :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
reconsider x = a, y = b, z = c as Element of L by Defx1, TARSKI:def 3;
( b "/\" c = y "/\" z & a "\/" b = x "\/" y & a "\/" c = x "\/" z ) by Thx3, Thx4;
then ( a "\/" (b "/\" c) = x "\/" (y "/\" z) & (a "\/" b) "/\" (a "\/" c) = (x "\/" y) "/\" (x "\/" z) ) by Thx3, Thx4;
hence a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by Z3; :: thesis: verum
end;