let L be non empty LattStr ; :: thesis: ( L is join-commutative & L is join-associative & L is meet-commutative & L is meet-associative & ( for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ) & ( for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ) implies ( ( for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) ) )
assume A2: L is join-commutative ; :: thesis: ( not L is join-associative or not L is meet-commutative or not L is meet-associative or ex v1, v0 being Element of L st not v0 "/\" (v0 "\/" v1) = v0 or ex v1, v0 being Element of L st not v0 "\/" (v0 "/\" v1) = v0 or ( ( for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) ) )
assume A3: L is join-associative ; :: thesis: ( not L is meet-commutative or not L is meet-associative or ex v1, v0 being Element of L st not v0 "/\" (v0 "\/" v1) = v0 or ex v1, v0 being Element of L st not v0 "\/" (v0 "/\" v1) = v0 or ( ( for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) ) )
assume A4: L is meet-commutative ; :: thesis: ( not L is meet-associative or ex v1, v0 being Element of L st not v0 "/\" (v0 "\/" v1) = v0 or ex v1, v0 being Element of L st not v0 "\/" (v0 "/\" v1) = v0 or ( ( for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) ) )
assume A5: L is meet-associative ; :: thesis: ( ex v1, v0 being Element of L st not v0 "/\" (v0 "\/" v1) = v0 or ex v1, v0 being Element of L st not v0 "\/" (v0 "/\" v1) = v0 or ( ( for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) ) )
assume A6: for v1, v0 being Element of L holds v0 "/\" (v0 "\/" v1) = v0 ; :: thesis: ( ex v1, v0 being Element of L st not v0 "\/" (v0 "/\" v1) = v0 or ( ( for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) ) )
assume A7: for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 ; :: thesis: ( ( for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) )
thus for v1, v2, v0 being Element of L holds v0 "\/" (v1 "/\" (v0 "/\" v2)) = v0 :: thesis: ( ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) & ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) ) thus for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 :: thesis: ( ( for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ) ) thus for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 :: thesis: for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 let v2, v1, v0 be Element of L; :: thesis: ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1
((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = (v0 "\/" v1) "/\" ((v1 "\/" v2) "/\" v1) by A5
.= (v0 "\/" v1) "/\" (v1 "/\" (v1 "\/" v2)) by A4
.= (v0 "\/" v1) "/\" v1 by A6
.= v1 "/\" (v0 "\/" v1) by A4
.= v1 "/\" (v1 "\/" v0) by A2
.= v1 by A6 ;
hence ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" v1 = v1 ; :: thesis: verum