take L1 = QLTLattice1 ; :: thesis: ex L2 being QuasiLattice st
( the carrier of L1 = the carrier of L2 & the L_join of L1 = the L_join of L2 & the L_meet of L1 <> the L_meet of L2 )
take L2 = QLTLattice2 ; :: thesis: ( the carrier of L1 = the carrier of L2 & the L_join of L1 = the L_join of L2 & the L_meet of L1 <> the L_meet of L2 )
thus the carrier of L1 = the carrier of L2 ; :: thesis: ( the L_join of L1 = the L_join of L2 & the L_meet of L1 <> the L_meet of L2 )
thus the L_join of L1 = the L_join of L2 ; :: thesis: the L_meet of L1 <> the L_meet of L2
thus the L_meet of L1 <> the L_meet of L2 by WazneQLT7; :: thesis: verum